blob: dd9f3c07ac976f015576a94979bff806b7180a04 (
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
|
About or_introl.
Print or_introl.
Print Implicit or_introl.
Print eq_refl.
About eq_refl.
Print Implicit eq_refl.
Print plus.
About plus.
Print Implicit plus.
About plus_n_O.
Implicit Arguments le_S [[n] m].
Print le_S.
About comparison.
Print comparison.
Definition foo := forall x, x = 0.
Parameter bar : foo.
Implicit Arguments bar [x].
About bar.
Print bar.
About Peano. (* Module *)
About existS2. (* Notation *)
Implicit Arguments eq_refl [[A] [x]] [[A]].
Print eq_refl.
|
