Formalizing TaPL

あきるor諦めるまでTaPLを定理証明支援系で形式化をします。
使用言語：Coq, Lean3
パーサー付きのものもある。
〜chap8　：The Coq Proof Assistant:version 8.11.2
chap9〜10：The Coq Proof Assistant:version 8.12.0
chap11〜 ：The Coq Proof Assistant:version 8.13.0

• Chap.3(arith)
• Chap.4(arith)
• Chap.5(untype_lambda)
• Chap.6(untype_lambda)
• Chap.7(untype_lambda)(他のリポジトリでやった)
• Chap.8(typeArith)
• Chap.9(hastype_lambda/typeLambda_string)(パーサーなし)
• Chap.10(hastype_lambda/deBruijn)(パーサーなし)
• Chap.11(fullsimpl/chap11)(パーサーなし)
• Chap.22(recon/)(パーサーなし)
• Chap.23(systemF/chap23.v)