Chapter4を読み進める。 Include "../lib/plus.g". Classify induction(n:nat) return Forall(m:nat). { (plus n (S m)) = (S (plus n m)) } with Z => foralli(m:nat). trans cong (plus * (S m)) n_eq trans join (plus Z (S m)) (S (plus Z m)) cong (S (…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。