blob: 62aa80f8ab96da0079f3ca0896d2f9711f6a26ab (
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
|
About existT.
Print existT.
Print Implicit existT.
Print eq_refl.
About eq_refl.
Print Implicit eq_refl.
Print Nat.add.
About Nat.add.
Print Implicit Nat.add.
About plus_n_O.
Arguments le_S {n} [m] _.
Print le_S.
About comparison.
Print comparison.
Definition foo := forall x, x = 0.
Parameter bar : foo.
Arguments bar [x].
About bar.
Print bar.
About Peano. (* Module *)
About sym_eq. (* Notation *)
Arguments eq_refl {A} {x}, {A} x.
Print eq_refl.
Definition newdef := fun x:nat => x.
Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
intros n h h'.
About n. (* search hypothesis *)
About h. (* search hypothesis *)
Abort.
Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False.
intros n g h h'.
About g. (* search hypothesis *)
About h. (* search hypothesis *)
Abort.
|
