Print eq. (* ===> Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x *)eq_reflは引数を持たないコンストラクタ。 eq_reflを実行すると、なんらかの型Aの値xを取って、 eq x x (x = x)という命題型の値(つまり証明or根拠)を返す関数?を返す…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。