Coq 定理証明 のための言語 参考文献 Coqを用いた『解析入門』の証明 - くたくたじゅうよん Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明 PDF Tactic Index tactic reference CoqIdeを使ってみる 2021-09-08 型付きラムダ計算の強正規化定理の形式化 Simply Typed Lambda Calculus, System F の強正規化定理を Coq で形式化した