1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
(* coq-prog-args: ("-impredicative-set") *)
Set Implicit Arguments.
Unset Strict Implicit.
Module Type SIG.
Parameter id : forall A : Set, A -> A.
End SIG.
Module M (X: SIG).
Definition idid := X.id X.id.
Definition id := idid X.id.
End M.
Module N := M.
Module Nat.
Definition T := nat.
Definition x := 0.
Definition id (A : Set) (x : A) := x.
End Nat.
Module Z := N Nat.
Check (Z.idid 0).
Module P (Y: SIG) := N.
Module Y := P Nat Z.
Check (Y.id 0).
|
