blob: 84942da188a1a84d59701fbeadf35b4f38a9bc5c (
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
|
Module 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.
End M.
(*Lemma w1 : (M.rel O (S O)).
Auto.
*)
Import M.
Print Hint *.
Lemma w1 : (O#(S O)).
Print Hint.
Print Hint *.
Auto.
Save.
Check (O#O).
Locate rel.
Locate Library M.
Module N:=Top.M.
|
