blob: 2b1c5e8436b1a95428fe275dbc692d608b31073f [file] [edit]
1079.lean:4:2-6:12: error: alternative 'isFalse' has not been provided
[Meta.Tactic.simp.rewrite] h:1000, m ==> n
[Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
?a = ?a
with
Ordering.eq = Ordering.lt
[Meta.Tactic.simp.rewrite] imp_self:10000, False → False ==> True