• TODO(ここに説明が来る)

• 保存機能等が現時点ではありませんので気をつけください

• パースエラーは現状画面下部にスクロールすることで確認できます

• パースは停止する確証があります。型付けと評価は停止するはずではありますが、無限ループっぽい挙動やパターンを見つけましたら教えていただけますと幸いです。

• 現時点で、 nat_indのような帰納法を導入するために等価性の公理と共に導入する方法がありません

型付け結果

評価の結果

パースの結果

パース時の警告・エラーなど

なし

参考

• Types and Programming Languages B. Pierce. MIT Press, 2002.
• Advanced Topics in Types and Programming Languages B. Pierce. MIT Press, 2005.
• The Calculus of Constructions T. Coquand and G. Huet. In Information and Computation, 76(2/3):95–120, 1988.
  • 型部分のみを評価するよう限定した場合の停止性の解析方法が紹介されている。 これを項も評価するようにした場合に応用する方法が自分では分からなかった。 誰かわかる方いらっしゃいましたらご教示くださいますと幸いです。
• Calculus of constructions - Wikipedia