22c8154811
See new test for example that takes exponential time without new simp theorems. TODO: replace auxiliary theorems with simprocs as soon as we implement them.
18 lines
717 B
Text
18 lines
717 B
Text
1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
|
|
[Meta.Tactic.simp.discharge] >> discharge?: m = n
|
|
[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
|
|
?a = ?a
|
|
with
|
|
m = n
|
|
[Meta.Tactic.simp.unify] Nat.succ.injEq:1000, failed to unify
|
|
Nat.succ ?n = Nat.succ ?n
|
|
with
|
|
m = n
|
|
[Meta.Tactic.simp.rewrite] h:1000, m ==> n
|
|
[Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
|
|
[Meta.Tactic.simp.rewrite] @ite_cond_true:1000, if m = n then Ordering.eq else Ordering.gt ==> Ordering.eq
|
|
[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
|
|
?a = ?a
|
|
with
|
|
Ordering.eq = Ordering.lt
|
|
[Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True
|