blob: 3419d5ac629deda1c51a520e942346af1141d083 (
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(* Some tests of the Search command *)
Search le. (* app nodes *)
Search bool. (* no apps *)
Search (@eq nat). (* complex pattern *)
Search (@eq _ _ true).
Search (@eq _ _ _) true -false. (* andb_prop *)
Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *)
Definition newdef := fun x:nat => x.
Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
cut False.
intros _ n h h'.
Search n. (* search hypothesis *)
Search newdef. (* search hypothesis *)
Search ( _ <> newdef _). (* search hypothesis, pattern *)
Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *)
1:Search newdef.
2:Search newdef.
Fail 3:Search newdef.
Fail 1-2:Search newdef.
Fail all:Search newdef.
Abort.
Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
intros n P h h'.
Search P. (* search hypothesis also for patterns *)
Search (P _). (* search hypothesis also for patterns *)
Search (P n). (* search hypothesis also for patterns *)
Search (P _) -"h'". (* search hypothesis also for patterns *)
Search (P _) -not. (* search hypothesis also for patterns *)
Abort.
Module M.
Section S.
Variable A:Type.
Variable a:A.
Theorem Thm (b:A) : True.
Search A. (* Test search in hypotheses *)
Abort.
End S.
End M.
(* Reproduce the example of the doc *)
Reset Initial.
Search "_assoc".
Search "+".
Search hyp:bool -headhyp:bool.
Search concl:bool -headconcl:bool.
Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
Require Import PeanoNat.
Search (_ ?n ?m = _ ?m ?n).
Search "'mod'" -"mod".
Search "mod"%nat -"mod".
Reset Initial.
Require Import Morphisms.
Search is:Instance [ Reflexive | Symmetric ].
Module Bug12525.
(* This was revealing a kernel bug with delta-resolution *)
Module A. Axiom a:Prop. Axiom b:a. End A.
Module B. Include A. End B.
Module M.
Search B.a.
End M.
End Bug12525.
From Coq Require Lia.
Module Bug12647.
(* Similar to #12525 *)
Module Type Foo.
Axiom P : nat -> Prop.
Axiom L : P 0.
End Foo.
Module Bar (F : Foo).
Search F.P.
End Bar.
End Bug12647.
Module WithCoercions.
Search headconcl:(_ + _) inside Datatypes.
Coercion Some_nat := @Some nat.
Axiom f : None = 0.
Search (None = 0).
End WithCoercions.
Require Import List.
Module Wish13349.
Search partition "1" inside List.
End Wish13349.
|
