diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean index 891f03e4f..817046225 100644 --- a/Aesop/Builder/Apply.lean +++ b/Aesop/Builder/Apply.lean @@ -6,6 +6,7 @@ Authors: Jannis Limperg module public import Aesop.Builder.Basic +import Batteries.Lean.Expr public section diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean index 7e75a6e9e..2ad7003a5 100644 --- a/Aesop/Builder/Cases.lean +++ b/Aesop/Builder/Cases.lean @@ -7,6 +7,7 @@ module public import Aesop.Builder.Basic public import Aesop.RuleTac.Cases +import Batteries.Lean.Expr public section diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 83feedab1..92e2f68ea 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -28,7 +28,7 @@ namespace RuleBuilder def getForwardIndexingMode (type : Expr) (immediate : UnorderedArraySet PremiseIndex) : MetaM IndexingMode := do - let immediate := immediate.toArray.map (·.toNat) + let immediate := immediate.toArray.map PremiseIndex.toNat match immediate.max? with | some i => withoutModifyingState do diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean index 71e039e35..e70736bcf 100644 --- a/Aesop/BuiltinRules/DestructProducts.lean +++ b/Aesop/BuiltinRules/DestructProducts.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +public meta import Lean.Meta.Tactic.Apply public import Aesop.Frontend.Attribute public import Aesop.Frontend.Extension public import Aesop.Frontend.RuleExpr diff --git a/Aesop/ElabM.lean b/Aesop/ElabM.lean index a139c4cb2..63edae9d4 100644 --- a/Aesop/ElabM.lean +++ b/Aesop/ElabM.lean @@ -5,7 +5,10 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Expr +public import Lean.Meta.Basic +public import Lean.Elab.Term.TermElabM public section diff --git a/Aesop/Exception.lean b/Aesop/Exception.lean index fa0d891aa..c9e4b50cd 100644 --- a/Aesop/Exception.lean +++ b/Aesop/Exception.lean @@ -5,7 +5,7 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean.Exception public section diff --git a/Aesop/Forward/Match.lean b/Aesop/Forward/Match.lean index 5efcd179e..ac521c1a0 100644 --- a/Aesop/Forward/Match.lean +++ b/Aesop/Forward/Match.lean @@ -5,6 +5,7 @@ Authors: Xavier Généreux, Jannis Limperg -/ module +import Lean.Meta.Tactic.Apply public import Aesop.Forward.Match.Types public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex @@ -14,9 +15,8 @@ public import Aesop.RuleTac.Descr public import Aesop.RuleTac.ElabRuleTerm public import Aesop.RuleTac.Forward.Basic public import Aesop.Script.SpecificTactics -public import Batteries.Lean.Meta.UnusedNames +import Batteries.Lean.Meta.UnusedNames public import Aesop.Util.Basic -public import Lean public section diff --git a/Aesop/Forward/RuleInfo.lean b/Aesop/Forward/RuleInfo.lean index cf31c14df..a6dcef131 100644 --- a/Aesop/Forward/RuleInfo.lean +++ b/Aesop/Forward/RuleInfo.lean @@ -10,6 +10,7 @@ public import Aesop.Forward.SlotIndex public import Aesop.RulePattern public import Aesop.Util.Basic public import Aesop.Util.UnionFind +public import Batteries.Data.Array.Basic public section diff --git a/Aesop/Frontend/Basic.lean b/Aesop/Frontend/Basic.lean index 4ef121244..89ca55575 100644 --- a/Aesop/Frontend/Basic.lean +++ b/Aesop/Frontend/Basic.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Exception +public import Lean.Elab.Exception public section diff --git a/Aesop/Frontend/Command.lean b/Aesop/Frontend/Command.lean index e7fe401d2..ce96ea74f 100644 --- a/Aesop/Frontend/Command.lean +++ b/Aesop/Frontend/Command.lean @@ -78,7 +78,7 @@ elab_rules : command def evalStatsReport? (name : Name) : CoreM (Option StatsReport) := do try - unsafe evalConstCheck StatsReport ``StatsReport name + unsafe some <$> evalConstCheck StatsReport ``StatsReport name catch _ => return none diff --git a/Aesop/Frontend/Tactic.lean b/Aesop/Frontend/Tactic.lean index eb0a61f64..f4b4bef9e 100644 --- a/Aesop/Frontend/Tactic.lean +++ b/Aesop/Frontend/Tactic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Frontend.RuleExpr public import Aesop.Options public import Batteries.Linter.UnreachableTactic diff --git a/Aesop/Index.lean b/Aesop/Index.lean index 6f276ca24..fbfb46107 100644 --- a/Aesop/Index.lean +++ b/Aesop/Index.lean @@ -12,8 +12,8 @@ public import Aesop.RulePattern public import Aesop.Rule.Basic public import Aesop.Tracing public import Batteries.Lean.Meta.InstantiateMVars -public import Batteries.Lean.PersistentHashSet -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.PersistentHashSet +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Index/DiscrTreeConfig.lean b/Aesop/Index/DiscrTreeConfig.lean index 1e7146592..7994bd61e 100644 --- a/Aesop/Index/DiscrTreeConfig.lean +++ b/Aesop/Index/DiscrTreeConfig.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Basic +public import Lean.Meta.DiscrTree.Types public section diff --git a/Aesop/Index/Forward.lean b/Aesop/Index/Forward.lean index ad15d0759..565797c00 100644 --- a/Aesop/Index/Forward.lean +++ b/Aesop/Index/Forward.lean @@ -8,7 +8,7 @@ module public import Aesop.Forward.Match.Types public import Aesop.Rule.Forward public import Aesop.Index.Basic -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Index/RulePattern.lean b/Aesop/Index/RulePattern.lean index aea54dbd5..6681ce565 100644 --- a/Aesop/Index/RulePattern.lean +++ b/Aesop/Index/RulePattern.lean @@ -8,7 +8,7 @@ module public import Aesop.Index.Basic public import Aesop.Util.OrderedHashSet public import Aesop.RuleTac.GoalDiff -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean index 0e8352d27..9646121a0 100644 --- a/Aesop/Options/Public.lean +++ b/Aesop/Options/Public.lean @@ -1,6 +1,7 @@ module -public import Lean +import Lean +public import Lean.Data.Options public section diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean index 66b338064..887ccabbd 100644 --- a/Aesop/RuleSet.lean +++ b/Aesop/RuleSet.lean @@ -10,6 +10,8 @@ public import Aesop.Index.Forward public import Aesop.RuleSet.Filter public import Aesop.RuleSet.Member public import Aesop.Tree.Data.ForwardRuleMatches +import Batteries.Lean.PersistentHashMap +import Batteries.Lean.PersistentHashSet public section diff --git a/Aesop/RuleSet/Name.lean b/Aesop/RuleSet/Name.lean index 62c5792e6..9de22f5c3 100644 --- a/Aesop/RuleSet/Name.lean +++ b/Aesop/RuleSet/Name.lean @@ -5,7 +5,7 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean public section diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index d3d69eaa8..c68ea47ff 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -13,7 +13,6 @@ public import Aesop.RuleTac.GoalDiff public import Aesop.RuleTac.FVarIdSubst public import Aesop.Script.CtorNames public import Aesop.Script.Step -public import Batteries.Lean.Meta.SavedState public import Aesop.Options.Internal public section diff --git a/Aesop/RuleTac/ElabRuleTerm.lean b/Aesop/RuleTac/ElabRuleTerm.lean index 55535d1c7..b8d509462 100644 --- a/Aesop/RuleTac/ElabRuleTerm.lean +++ b/Aesop/RuleTac/ElabRuleTerm.lean @@ -5,6 +5,10 @@ Authors: Jannis Limperg -/ module +import Lean +public import Lean.Elab.Tactic.Basic +public import Lean.Meta.Tactic.Simp.Types +public import Lean.Meta.Tactic.Simp.Simproc public import Aesop.ElabM public section diff --git a/Aesop/RuleTac/FVarIdSubst.lean b/Aesop/RuleTac/FVarIdSubst.lean index 8f0130d6c..5b4595fb8 100644 --- a/Aesop/RuleTac/FVarIdSubst.lean +++ b/Aesop/RuleTac/FVarIdSubst.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Std.Data.HashMap.Basic +public import Lean.Meta.Tactic.FVarSubst public section diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 4e031c64a..c9c19a819 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -5,12 +5,13 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Forward.Match public import Aesop.RuleTac.Basic public import Aesop.RuleTac.ElabRuleTerm public import Aesop.RuleTac.Forward.Basic public import Aesop.Script.SpecificTactics -public import Batteries.Lean.Meta.UnusedNames +import Batteries.Lean.Meta.UnusedNames public section diff --git a/Aesop/RuleTac/Forward/Basic.lean b/Aesop/RuleTac/Forward/Basic.lean index 0d5038afb..56f08a3a3 100644 --- a/Aesop/RuleTac/Forward/Basic.lean +++ b/Aesop/RuleTac/Forward/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Util.Basic public import Aesop.Util.EqualUpToIds diff --git a/Aesop/Saturate.lean b/Aesop/Saturate.lean index 880e44446..a4e28d400 100644 --- a/Aesop/Saturate.lean +++ b/Aesop/Saturate.lean @@ -11,7 +11,7 @@ public import Aesop.RuleSet public import Aesop.RuleTac public import Aesop.Search.Expansion.Basic public import Aesop.Script.Check -public import Batteries.Data.BinomialHeap.Basic +import Batteries.Data.BinomialHeap.Basic public section @@ -124,7 +124,7 @@ where namespace Stateful -abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le +private abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le partial def saturateCore (rs : LocalRuleSet) (goal : MVarId) : SaturateM MVarId := withExceptionPrefix "saturate: internal error: " do diff --git a/Aesop/Script/CtorNames.lean b/Aesop/Script/CtorNames.lean index 34a0dd308..2e2826dc6 100644 --- a/Aesop/Script/CtorNames.lean +++ b/Aesop/Script/CtorNames.lean @@ -1,5 +1,6 @@ module +public import Lean.Meta.Tactic.Induction public import Aesop.Util.Basic public section diff --git a/Aesop/Script/GoalWithMVars.lean b/Aesop/Script/GoalWithMVars.lean index 48a13ab4a..ede01d73e 100644 --- a/Aesop/Script/GoalWithMVars.lean +++ b/Aesop/Script/GoalWithMVars.lean @@ -1,6 +1,7 @@ module -public import Lean +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Script/Main.lean b/Aesop/Script/Main.lean index e4cc6d05f..f01fbae34 100644 --- a/Aesop/Script/Main.lean +++ b/Aesop/Script/Main.lean @@ -11,6 +11,7 @@ public import Aesop.Script.StructureStatic public import Aesop.Script.OptimizeSyntax public import Aesop.Stats.Basic public import Aesop.Options.Internal +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/OptimizeSyntax.lean b/Aesop/Script/OptimizeSyntax.lean index f580dc2cb..653645076 100644 --- a/Aesop/Script/OptimizeSyntax.lean +++ b/Aesop/Script/OptimizeSyntax.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Std.Data.HashSet.Basic public section diff --git a/Aesop/Script/SScript.lean b/Aesop/Script/SScript.lean index c306bf3d0..2b0aa0fcd 100644 --- a/Aesop/Script/SScript.lean +++ b/Aesop/Script/SScript.lean @@ -1,6 +1,7 @@ module public import Aesop.Script.Step +import Batteries.Tactic.PermuteGoals public section diff --git a/Aesop/Script/SpecificTactics.lean b/Aesop/Script/SpecificTactics.lean index 8ff45503c..ac16f310d 100644 --- a/Aesop/Script/SpecificTactics.lean +++ b/Aesop/Script/SpecificTactics.lean @@ -5,13 +5,15 @@ Authors: Jannis Limperg -/ module +import Lean +public import Lean.Meta.Tactic.Cases public import Aesop.Util.Tactic public import Aesop.Util.Tactic.Ext public import Aesop.Util.Tactic.Unfold public import Aesop.Util.Unfold public import Aesop.Script.CtorNames public import Aesop.Script.ScriptM -public import Batteries.Lean.Meta.Inaccessible +import Batteries.Lean.Meta.Inaccessible public section diff --git a/Aesop/Script/Step.lean b/Aesop/Script/Step.lean index 227b2c89a..257cb9d21 100644 --- a/Aesop/Script/Step.lean +++ b/Aesop/Script/Step.lean @@ -10,7 +10,8 @@ public import Aesop.Script.Tactic public import Aesop.Script.TacticState public import Aesop.Script.Util public import Aesop.Tracing -public import Batteries.Tactic.PermuteGoals +import Batteries.Tactic.PermuteGoals +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index 9786b7495..bc83dd6ec 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -10,6 +10,7 @@ public import Aesop.Script.UScriptToSScript public import Aesop.Script.Util public import Aesop.Script.SScript public import Aesop.Tracing +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/Tactic.lean b/Aesop/Script/Tactic.lean index e0d4849d2..ac3a45799 100644 --- a/Aesop/Script/Tactic.lean +++ b/Aesop/Script/Tactic.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Script/TacticState.lean b/Aesop/Script/TacticState.lean index 28d1402da..299b0c544 100644 --- a/Aesop/Script/TacticState.lean +++ b/Aesop/Script/TacticState.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Batteries.Lean.Meta.Basic +import Lean +import Batteries.Lean.Meta.Basic public import Aesop.Script.GoalWithMVars public section diff --git a/Aesop/Script/UScript.lean b/Aesop/Script/UScript.lean index d638db983..91e720bbe 100644 --- a/Aesop/Script/UScript.lean +++ b/Aesop/Script/UScript.lean @@ -6,6 +6,7 @@ Authors: Jannis Limperg module public import Aesop.Script.Step +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean index 440276eeb..055d3c263 100644 --- a/Aesop/Script/Util.lean +++ b/Aesop/Script/Util.lean @@ -7,7 +7,7 @@ module public import Aesop.Util.Basic public import Aesop.Util.EqualUpToIds -public import Batteries.Lean.Meta.SavedState +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean index 697e93ee4..941e41ae0 100644 --- a/Aesop/Search/Expansion/Norm.lean +++ b/Aesop/Search/Expansion/Norm.lean @@ -14,7 +14,8 @@ public import Aesop.Search.Expansion.Simp public import Aesop.Search.RuleSelection public import Aesop.Search.SearchM public import Aesop.Tree.State -public import Batteries.Lean.HashSet +import Batteries.Lean.HashSet +public import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean index 4cab9d4e3..ec9f4556e 100644 --- a/Aesop/Tracing.lean +++ b/Aesop/Tracing.lean @@ -6,7 +6,6 @@ Authors: Jannis Limperg module public import Aesop.Util.Basic -public import Batteries.Data.Array.Basic public import Lean.Elab.Term public import Lean.Meta.Tactic.Simp @@ -110,7 +109,7 @@ macro "aesop_trace![" opt:ident "] " msg:(interpolatedStr(term) <|> term) : `(doElem| Lean.addTrace (Aesop.TraceOption.traceClass $opt) $msg) macro "aesop_trace[" opt:ident "] " - msg:(interpolatedStr(term) <|> Parser.Term.do <|> term) : doElem => do + msg:(interpolatedStr(term) <|> term) : doElem => do let msg := msg.raw let opt ← mkIdent <$> resolveTraceOption opt match msg with diff --git a/Aesop/Tree/AddRapp.lean b/Aesop/Tree/AddRapp.lean index 9bda8e2c1..d20bc1ea8 100644 --- a/Aesop/Tree/AddRapp.lean +++ b/Aesop/Tree/AddRapp.lean @@ -10,6 +10,7 @@ public import Aesop.Forward.State.ApplyGoalDiff public import Aesop.Tree.Traversal public import Aesop.Tree.TreeM public import Aesop.Util.UnionFind +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/Check.lean b/Aesop/Tree/Check.lean index 58a820200..537d90194 100644 --- a/Aesop/Tree/Check.lean +++ b/Aesop/Tree/Check.lean @@ -9,8 +9,9 @@ public import Aesop.Check public import Aesop.Tree.State public import Aesop.Tree.Traversal public import Aesop.Tree.TreeM -public import Batteries.Lean.HashSet public import Aesop.Tree.RunMetaM +import Batteries.Lean.HashSet +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/ExtractProof.lean b/Aesop/Tree/ExtractProof.lean index e1f50da63..52a247891 100644 --- a/Aesop/Tree/ExtractProof.lean +++ b/Aesop/Tree/ExtractProof.lean @@ -8,7 +8,8 @@ module public import Lean.Replay public import Aesop.Tracing public import Aesop.Tree.TreeM -public import Batteries.Lean.Meta.InstantiateMVars +import Batteries.Lean.Meta.InstantiateMVars +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/Tracing.lean b/Aesop/Tree/Tracing.lean index e51bf8827..98c1e17b9 100644 --- a/Aesop/Tree/Tracing.lean +++ b/Aesop/Tree/Tracing.lean @@ -2,6 +2,7 @@ module public import Aesop.Tree.RunMetaM public import Aesop.Tracing +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 37ea41a2d..f8e2c3b96 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -8,9 +8,11 @@ module public import Aesop.Index.DiscrTreeConfig public import Aesop.Nanos public import Aesop.Util.UnorderedArraySet -public import Batteries.Lean.Expr -public import Batteries.Data.String.Basic -public import Lean +import Lean +public import Lean.Meta.DiscrTree.Util +public import Lean.Meta.Tactic.Simp.SimpTheorems +public import Lean.Util.ForEachExpr +public import Lean.Elab.Tactic.Basic public import Std.Data.HashSet.Basic public section diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean index b1e3b4956..db5aeb9ba 100644 --- a/Aesop/Util/Tactic.lean +++ b/Aesop/Util/Tactic.lean @@ -5,8 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean -public import Batteries.Tactic.OpenPrivate +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Util/Tactic/Ext.lean b/Aesop/Util/Tactic/Ext.lean index d8ced83d0..aee2c3c7e 100644 --- a/Aesop/Util/Tactic/Ext.lean +++ b/Aesop/Util/Tactic/Ext.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Tracing public section diff --git a/Aesop/Util/Tactic/Unfold.lean b/Aesop/Util/Tactic/Unfold.lean index 3fb6e5f9b..7081571c4 100644 --- a/Aesop/Util/Tactic/Unfold.lean +++ b/Aesop/Util/Tactic/Unfold.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +public import Lean.Elab.Tactic.Basic public meta import Aesop.Util.Unfold public section diff --git a/Aesop/Util/Unfold.lean b/Aesop/Util/Unfold.lean index 1c86afb05..81da7b531 100644 --- a/Aesop/Util/Unfold.lean +++ b/Aesop/Util/Unfold.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Tactic.Simp.Main public section diff --git a/AesopTest/EqualUpToIds.lean b/AesopTest/EqualUpToIds.lean index 2a8691777..ba4f78294 100644 --- a/AesopTest/EqualUpToIds.lean +++ b/AesopTest/EqualUpToIds.lean @@ -8,6 +8,8 @@ import Aesop.Util.Basic import Aesop.Util.EqualUpToIds import Aesop.Tree.RunMetaM +set_option linter.unreachableTactic false + -- Some simple test cases for the EqualUpToIds module. The module is mostly -- tested by using it in script validation, which is run on almost all Aesop -- calls in the test suite. diff --git a/AesopTest/IncompleteScript.lean b/AesopTest/IncompleteScript.lean index 38d814372..bf34238d1 100644 --- a/AesopTest/IncompleteScript.lean +++ b/AesopTest/IncompleteScript.lean @@ -57,7 +57,6 @@ info: Try this: warning: aesop: failed to prove the goal after exhaustive search. --- error: unsolved goals -case a.a ⊢ Even 1 -/ #guard_msgs in diff --git a/AesopTest/List.lean b/AesopTest/List.lean index 5963d9032..f1856ebb2 100644 --- a/AesopTest/List.lean +++ b/AesopTest/List.lean @@ -178,7 +178,7 @@ theorem subset_trans {l₁ l₂ l₃ : List α} : l₁ ⊆ l₂ → l₂ ⊆ l -- END PRELUDE -instance unique_of_is_empty [IsEmpty α] : Unique (List α) := by +def unique_of_is_empty [IsEmpty α] : Unique (List α) := by aesop (add 1% cases List) -- instance : is_left_id (list α) has_append.append [] := diff --git a/AesopTest/SafePrefixExpansionRappLimit.lean b/AesopTest/SafePrefixExpansionRappLimit.lean index b8a4e82be..3dd6927de 100644 --- a/AesopTest/SafePrefixExpansionRappLimit.lean +++ b/AesopTest/SafePrefixExpansionRappLimit.lean @@ -15,7 +15,6 @@ warning: aesop: failed to prove the goal. Some goals were not explored because t warning: aesop: safe prefix was not fully expanded because the maximum number of rule applications (50) was reached. --- error: unsolved goals -case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a ⊢ False -/ #guard_msgs in @@ -27,7 +26,6 @@ error: tactic 'aesop' failed, failed to prove the goal. Some goals were not expl Initial goal: ⊢ False Remaining goals after safe rules: - case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a ⊢ False The safe prefix was not fully expanded because the maximum number of rule applications (50) was reached. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 01995249d..b7f6fa99b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "81c23850e7c2b5f82ed16e3569def2fe0f52e1c9", + "rev": "26a07f000f8c9fb51754dd848ef72422442e7b32", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-13305", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index e545e3e0b..7822d9676 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "nightly-testing" +rev = "lean-pr-testing-13305" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 6fd0431c6..9c4d8d76f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-06 \ No newline at end of file +leanprover/lean4-pr-releases:pr-release-13305-6b53385