自分が理解したであろうところの証明オブジェクトの書き方。 XXX -> YYY := fun (H : XXX) => (fun (H1 : YYY) => H1) (← ここで YYY型の変数H1を返す関数を生成してそのまま実行。 ... YYY型の変数 を組み立てる何かの処理 ... ←上の行の関数の実行に対し…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。