Gallina の構文と Vernacular コマンド

Gallina の構文と Vernacular コマンド 字句 空白文字、改行、タブは空白とみなされる。 コメントは (* で始まり *) で終わる。コメントの中に他のコメントあるいは文字列を入れることができる。コメントは空白とみなされる。 識別子には、英字 (A, B, …)、下線 (_) その他 Unicode で識別子として利用可能とされている文字が使える。識別子の二文字目以降には数字およびプライム (') も使える。 キーワード 特殊な意味を持つため識別子として使えないキーワードは以下の通り: _ as at cofix else end exists exists2 fix for forall fun if IF in let match mod Prop return Set then Type using where with 項 全称量化子 forall n, 0 fo

[yaotti]

syntax