diff --git a/AesopTest/HeartbeatLimit.lean b/AesopTest/HeartbeatLimit.lean index 77d61c1..0ea829d 100644 --- a/AesopTest/HeartbeatLimit.lean +++ b/AesopTest/HeartbeatLimit.lean @@ -8,6 +8,7 @@ import Aesop import Batteries.Linter.UnreachableTactic set_option aesop.check.all true +set_option aesop.smallErrorMessages true set_option linter.unreachableTactic false @[aesop safe constructors] @@ -15,16 +16,10 @@ inductive Even : Nat → Prop | zero : Even 0 | plusTwo : Even n → Even (n + 2) --- FIXME this is producing a different message under v4.11.0-rc1 - --- /-- --- error: (deterministic) timeout at `whnf`, maximum number of heartbeats (1) has been reached --- use `set_option maxHeartbeats ` to set the limit --- use `set_option diagnostics true` to get diagnostic information --- -/ --- #guard_msgs in --- example : Even 10 := by --- aesop (config := { maxRuleHeartbeats := 1, terminal := true }) +/-- error: tactic 'aesop' failed, failed to prove the goal after exhaustive search. -/ +#guard_msgs in +example : Even 10 := by + aesop (config := { maxRuleHeartbeats := 1, terminal := true }) example : Even 10 := by aesop