やはり先週詰ってたとこで詰まる。全称記号つき命題を特定の値を伴って関数に渡したりする場合がよくわかっておりません。 Inductive ev :nat -> Prop := | ev_O : ev O | ev_SS : forall n : nat, ev n -> ev (S (S n)).で、コンストラクタ関数 ev_SSに何が…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。