非常に奇妙な構文を見てきました: (name:type1) type2 in type および [name:type] expr in expression は、Pi と Lambda の代替構文のように見えますが、数時間検索した後、ドキュメントには何も見つかりませんでした。すべて無駄に。
それは何を意味し、どこで定義されていますか? (使用例へのリンクが失われてしまい申し訳ありません)
1 に答える
4
古いバージョンの Coq 用に書かれた理論を読んでいます。構文は V8.0 で大幅に刷新されました。V8.0 には、V7 の理論を V8 に変換するツールが同梱されていましたが、これは非常にうまく機能しました。ツールはその後のリリースから削除されました。
論文Translation from Coq V7 to V8で変更点のレビューを見ることができます。
特に、(a:b) cは全称量化であり、現在は と書かれていforall a:b, cます。[a:b] cはラムダ抽象化であり、現在は と書かれてfun a:b => cいます。古い理論を読むときのもう 1 つの重要なことは、関数適用には括弧が必要であり、優先順位が低かったということ(f x = y)です。(f (x=y))([x:nat]y z)(([x:nat]y) z)
于 2011-04-14T22:21:46.157 に答える