blob: 8183c67c6870367f13930e1e8ef16d7323f4605b (
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
|
Reset Initial.
Modtype SET.
Axiom T:Set.
Axiom x:T.
EndT SET.
Implicit Arguments On.
Mod M[X:SET].
Definition T := nat.
Definition x := O.
Definition f := [A:Set][x:A]X.x.
EndM M.
Mod N:=M.
Mod Nat.
Definition T := nat.
Definition x := O.
EndM Nat.
Mod Z:=(N Nat).
Check (Z.f O).
Mod P[Y:SET] := N.
Mod Y:=P Z Nat.
Check (Y.f O).
|
