blob: 58ae2a52df3a6f4c08f48f2ab5b53f3b490fc563 (
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
|
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.
Locate Module M.
(*Lemma w1 : (M.rel O (S O)).
Auto.
*)
Import M.
Lemma w1 : (O#(S O)).
Auto.
Save.
Check (O#O).
Locate rel.
Locate Module M.
Module N:=Top.M.
|
