blob: 9edfd825569f97544ec0b2a21add84455f5f8e18 (
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
|
(** Test of the different syntaxes of SearchAbout, in particular
with and without the [ ... ] delimiters *)
SearchAbout plus.
SearchAbout plus mult.
SearchAbout "plus_n".
SearchAbout plus "plus_n".
SearchAbout "*".
SearchAbout "*" "+".
SearchAbout plus inside Peano.
SearchAbout plus mult inside Peano.
SearchAbout "plus_n" inside Peano.
SearchAbout plus "plus_n" inside Peano.
SearchAbout "*" inside Peano.
SearchAbout "*" "+" inside Peano.
SearchAbout plus outside Peano Logic.
SearchAbout plus mult outside Peano Logic.
SearchAbout "plus_n" outside Peano Logic.
SearchAbout plus "plus_n" outside Peano Logic.
SearchAbout "*" outside Peano Logic.
SearchAbout "*" "+" outside Peano Logic.
SearchAbout -"*" "+" outside Logic.
SearchAbout -"*"%nat "+"%nat outside Logic.
SearchAbout [plus].
SearchAbout [plus mult].
SearchAbout ["plus_n"].
SearchAbout [plus "plus_n"].
SearchAbout ["*"].
SearchAbout ["*" "+"].
SearchAbout [plus] inside Peano.
SearchAbout [plus mult] inside Peano.
SearchAbout ["plus_n"] inside Peano.
SearchAbout [plus "plus_n"] inside Peano.
SearchAbout ["*"] inside Peano.
SearchAbout ["*" "+"] inside Peano.
SearchAbout [plus] outside Peano Logic.
SearchAbout [plus mult] outside Peano Logic.
SearchAbout ["plus_n"] outside Peano Logic.
SearchAbout [plus "plus_n"] outside Peano Logic.
SearchAbout ["*"] outside Peano Logic.
SearchAbout ["*" "+"] outside Peano Logic.
SearchAbout [-"*" "+"] outside Logic.
SearchAbout [-"*"%nat "+"%nat] outside Logic.
(** The example in the Reference Manual *)
Require Import ZArith.
SearchAbout Z.mul Z.add "distr".
SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
|
