diff --git a/AesopTest/EraseSimp.lean b/AesopTest/EraseSimp.lean index 2bf9d4fb..bd50d67a 100644 --- a/AesopTest/EraseSimp.lean +++ b/AesopTest/EraseSimp.lean @@ -6,6 +6,7 @@ Authors: Jannis Limperg import Aesop import Std.Tactic.GuardMsgs +import Std.Linter.UnreachableTactic set_option aesop.check.all true set_option aesop.smallErrorMessages true diff --git a/AesopTest/HeartbeatLimit.lean b/AesopTest/HeartbeatLimit.lean index f8eba73f..d784fe40 100644 --- a/AesopTest/HeartbeatLimit.lean +++ b/AesopTest/HeartbeatLimit.lean @@ -6,6 +6,7 @@ Authors: Jannis Limperg import Aesop import Std.Tactic.GuardMsgs +import Std.Linter.UnreachableTactic set_option aesop.check.all true set_option linter.unreachableTactic false