自分の Coq メモを晒してみる。 ■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もし…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。