我想定義一個提供身份和組成的類。除了其他有用的實例(List with nil and concatenation;與關係,好,身份和組合;-)),我想有一個函數實例。在Coq中有( - >)的顯式類型構造函數嗎?
鑑於
Class Cat (C0 : Type) (C1 : C0 -> C0 -> Type) :=
{ identity : forall a, C1 a a
; compose : forall {a b c : C0}, C1 b c -> C1 a b -> C1 a c
(* snip: some laws *)
}.
我希望能夠定義像
Instance Cat (->) := { ... }.
但在勒柯克運營商不一樣,一起想。首先我假設->
是一個符號,但Locate "_ -> _".
聲稱這是一個Unknown notation
。使用fun a b => a -> b
有點作品,但類型看起來很有趣。
> Check (identity nat).
identity nat
: (fun a b : Type => a -> b) nat nat
(同去的Eval compute in
,看來它並沒有簡化的類型。)我寧願更具可讀性identity nat : nat -> nat
。 (目前,這些類型對於我正在做的事情來說變得不可讀)
有沒有辦法讓'原始'->
或至少說服Coq給我更好的類型?
附註:我建立了很多代表評價語義Inductive
,那是我的目標是「正常」的編程語言的子集映射到勒柯克和背部,傳輸安全約束和做魔術。我不得不一遍又一遍地用不同的構造函數來證明相同的東西,並希望這能讓我證明一次又一次的東西。我認爲類別是抽象的正確方法。我在這裏包括這個筆記,以防萬一我錯了,也許有更好的方法來避免整個->
問題。
實際上,[Logic.v](https://gforge.inria.fr/scm/viewvc.php/trunk/theories/Init/Logic.v?view=markup&revision=15929&root=coq)定義了「符號」A - > B「:=(forall(_:A),B):type_scope。」 – minopret