File tree Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Expand file tree Collapse file tree 2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -84,15 +84,15 @@ Arguments bar {x}
84
84
Module Corelib.Init.Peano
85
85
Notation sym_eq := eq_sym
86
86
Expands to: Notation Corelib.Init.Logic.sym_eq
87
- Declared in library Corelib.Init.Logic, line 800 , characters 0-45
87
+ Declared in library Corelib.Init.Logic, line 835 , characters 0-45
88
88
89
89
eq_sym : forall [A : Type] [x y : A], x = y -> y = x
90
90
91
91
eq_sym is not universe polymorphic
92
92
Arguments eq_sym [A]%_type_scope [x y] _
93
93
eq_sym is transparent
94
94
Expands to: Constant Corelib.Init.Logic.eq_sym
95
- Declared in library Corelib.Init.Logic, line 443 , characters 12-18
95
+ Declared in library Corelib.Init.Logic, line 459 , characters 12-18
96
96
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
97
97
98
98
Arguments eq {A}%_type_scope x _
Original file line number Diff line number Diff line change @@ -8,7 +8,7 @@ nat_ind (fun n0 : nat => ((n0 * m) + n0) = (n0 * (S m)))
8
8
(let n0 := p * (S m) in
9
9
match H in _ = n1 return ((m + (p * m)) + (S p)) = (S (m + n1)) with
10
10
| eq_refl =>
11
- eq_Has_Leibniz_elim (fun n1 : nat => n1 = (S (m + ((p * m) + p))))
11
+ eq_Has_Leibniz_elimP (fun n1 : nat => n1 = (S (m + ((p * m) + p))))
12
12
(eq_S ((m + (p * m)) + p) (m + ((p * m) + p))
13
13
(nat_ind
14
14
(fun n1 : nat => ((n1 + (p * m)) + p) = (n1 + ((p * m) + p)))
You can’t perform that action at this time.
0 commit comments