blob: def6ed98dd314d1efef31ba2d7c5e3736150f239 (
plain)
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
Module Sylvain_Boulme.
Module Type Essai.
Parameter T: Type.
Parameter my_eq: T -> T -> Prop.
Parameter my_eq_refl: forall (x:T), (my_eq x x).
Parameter c: T.
End Essai.
Module Type Essai2.
Declare Module M: Essai.
Parameter c2: M.T.
End Essai2.
Module Type Essai3.
Declare Module M: Essai.
Parameter c3: M.T.
End Essai3.
Module Type Lift.
Declare Module Core: Essai.
Declare Module M: Essai.
Parameter lift: Core.T -> M.T.
Parameter lift_prop:forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
End Lift.
Module I2 (X:Essai) <: Essai2.
Module Core := X.
Module M<:Essai.
Definition T:Type :=Prop.
Definition my_eq:=(@eq Prop).
Definition c:=True.
Lemma my_eq_refl: forall (x:T), (my_eq x x).
Proof.
unfold my_eq; auto.
Qed.
End M.
Definition c2:=False.
Definition lift:=fun (_:Core.T) => M.c.
Definition lift_prop: forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
Proof.
unfold lift, M.my_eq; auto.
Qed.
End I2.
Module I4(X:Essai3) (L: Lift with Module Core := X.M) <: Essai3 with Module
M:=L.M.
Module M:=L.M.
Definition c3:=(L.lift X.c3).
End I4.
Module I5(X:Essai3).
Module Toto<: Lift with Module Core := X.M := I2(X.M).
Module E4<: Essai3 with Module M:=Toto.M := I4(X)(Toto).
(*
Le typage de E4 echoue avec le message
Error: Signature components for label my_eq_refl do not match
*)
Module E3<: Essai3 := I4(X)(Toto).
Definition zarb: forall (x:Toto.M.T), (Toto.M.my_eq x x) := E3.M.my_eq_refl.
End I5.
End Sylvain_Boulme.
Module Jacek.
Module Type SIG.
End SIG.
Module N.
Definition A:=Set.
End N.
Module Type SIG2.
Declare Module M:SIG.
Parameter B:Type.
End SIG2.
Module F(X:SIG2 with Module M:=N) (Y:SIG2 with Definition B:=X.M.A).
End F.
End Jacek.
Module anoun.
Module Type TITI.
Parameter X: Set.
End TITI.
Module Type Ex.
Declare Module t: TITI.
Parameter X : t.X -> t.X -> Set.
End Ex.
Module unionEx(X1: Ex) (X2:Ex with Module t :=X1.t): Ex.
Module t:=X1.t.
Definition X :=fun (a b:t.X) => ((X1.X a b)+(X2.X a b))%type.
End unionEx.
End anoun.
(* Le warning qui s'affiche lors de la compilation est le suivant :
TODO:replace module after with!
Est ce qu'il y'a qq1 qui pourrait m'aider à comprendre le probleme?!
Je vous remercie d'avance *)
|
