以下のように試した限りは、 関数の型に直接にソート (Type とか Set とか) を書けばそうなるけれど、 ちょっとでも型の書き方を複雑にするとそうならなくなってしまう感じかな (明示的に Arguments コマンドで設定することはできる)
ここで、x*y がふつうは自然数の乗算 (Nat.mul x y) なのだが、 type_scope では組を表現する型 (prod x y) なので、 その違いを使って引数の解釈を確認している
Fail Check @id (nat * nat). (* なんか動かない The term "nat" has type "Set" while it is expected to have type "nat". というエラーなので、x*y が Nat.mul と解釈されているようだ *) About id. (* Arguments id [A] _ と出てくる *) Definition id1 (A : Type) (x : A) := x. Check id1 (nat * nat). (* 自分で id と同じ定義をすると動く *) About id1. (* Arguments id1 _%type_scope _ と出てきて、第1引数が type_scope と解釈される設定になっているぽい *) (* Coq のソースの theories/Init/Datatypes.v では ID という型を定義して 使っているので、それを真似して定義してみる *) Definition ID2 := forall A:Type, A -> A. Definition id2 : ID2 := fun A x => x. Fail Check @id2 (nat * nat). (* これは id と同様に失敗する *) About id2. (* なぜかわからないが Arguments は出てこない *) Arguments id2 _%type_scope _. Check @id2 (nat * nat). (* 明示的に Arguments で設定すれば動く *) (* ID を展開してみる *) Definition id3 : forall A:Type, A -> A := fun A x => x. Check @id3 (nat * nat). (* これは動く *) About id3. (* Arguments id3 _%type_scope _ と出てくる *) (* Type というのを T という定数にしてみる *) Definition T := Type. Definition id4 : forall A:T, A -> A := fun A x => x. Fail Check @id4 (nat * nat). (* これは動かない *) About id4. (* なぜか Arguments はでてこない *) (* Type だけじゃなくて Set も試してみる *) Definition id5 : forall A:Set, A -> A := fun A x => x. Check @id5 (nat * nat). (* これは動く*)
なお、Coq 8.13.1 で試した
[latest]