- 490 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 11:17:47.41 ]
- スレチですまんのだけど、Coqだと
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x.
という風に等号を定義するだけで（ちなみに上記の意味は、「Type Aの変数xに対して
x=x（eq A x xのこと）の証明が存在することを仮定し、その証明をeq_reflと名づける」といった感じ。）
eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, eq A x y -> P y
というような等号公理が導かれてしまうけど、これってどういう原理なの？
わかりやすい説明とか文献あったら教えてくだされ。エラいひと！
