blob: ba333c525028558e4d5e559f7893f07cdd4e0561 (
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
|
Mod M.
Parameter rel:nat -> nat -> Prop.
Axiom w : (n:nat)(rel O (S n)).
Hints Resolve w.
Grammar constr constr8 :=
not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
Print Hint *.
Lemma w1 : (O#(S O)).
Auto.
Save.
EndM M.
(*Lemma w1 : (M.rel O (S O)).
Auto.
*)
Imp M.
Print Hint *.
Lemma w1 : (O#(S O)).
Print Hint.
Print Hint *.
Auto.
Save.
Check (O#O).
Locate rel.
Locate M.
Mod N:=Scratch.M.
|
