id関数 任意の型 A の引数をとり、それ自身を返す関数Coqは、 変数名 : 型 の順序でいろいろ宣言する。変数も、関数の引数も。 一番最初のもの。http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html Definition id (A : Type) (x : A) : A := x.型引数A (A…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。