blob: 627e109d5fbc0375ba64e1b060f376833f19b288 (
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
|
(** Test of the different syntaxes of Search *)
Search plus.
Search plus mult.
Search "plus_n".
Search plus "plus_n".
Search "*".
Search "*" "+".
Search plus inside Peano.
Search plus mult inside Peano.
Search "plus_n" inside Peano.
Search plus "plus_n" inside Peano.
Search "*" inside Peano.
Search "*" "+" inside Peano.
Search plus outside Peano Logic.
Search plus mult outside Peano Logic.
Search "plus_n" outside Peano Logic.
Search plus "plus_n" outside Peano Logic.
Search "*" outside Peano Logic.
Search "*" "+" outside Peano Logic.
Search -"*" "+" outside Logic.
Search -"*"%nat "+"%nat outside Logic.
(** The example in the Reference Manual *)
Require Import ZArith.
Search Z.mul Z.add "distr".
Search "+"%Z "*"%Z "distr" -positive -Prop.
Search (?x * _ + ?x * _)%Z outside Lia.
|
