CoqのマニュアルのTermの章を翻訳した
Coq v8.8.2 の Term の章を翻訳しました。
この章では Gallina の項の構成について説明しています。
恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔なので分かり易いです(それでも難しいんですが…)。
あと分かりにくいと言ったら型キャストの部分で、term <: type
とかterm <<: type
は項目が存在する割には全く説明が無いに等しいので何のことやら全然分かりません。これはヒドイ。
他に気になったところでは cofix
についての説明で、以下の説明に依るとこれは相互(構造)再帰ではないようなんですね。
The expression “fix ident1 ..." ... defined by mutual structural recursion. It is the local counterpart of the Fixpoint command.
https://coq.inria.fr/distrib/V8.8.2/refman/language/gallina-specification-language.html#recursive-functions
...
The expression “cofix ident1 ..." ... defined by a mutual guarded co-recursion. It is the local counterpart of the CoFixpoint command.
和訳した方では相互ガード付き余再帰としてありますがどうなんでしょう。
油断すると再帰と呼んでしまう気がしますね。