From a4a08d92be3de00def5298059bf707c72dfd3c66 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 19 Dec 2024 20:54:36 +1100 Subject: [PATCH] chore: remove unnecessary explicit indexing proofs (#185) --- Aesop/Builder/Forward.lean | 2 +- Aesop/RulePattern.lean | 6 +++--- Aesop/RuleTac/Forward.lean | 2 +- Aesop/Script/StructureDynamic.lean | 2 +- Aesop/Script/StructureStatic.lean | 2 +- Aesop/Script/Util.lean | 2 +- Aesop/Search/Expansion.lean | 2 +- 7 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 16b041d0..dd797435 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -60,7 +60,7 @@ def getImmediatePremises (type : Expr) (pat? : Option RulePattern) for h : i in [:args.size] do if isPatternInstantiated i then continue - let fvarId := (args[i]'h.2).fvarId! + let fvarId := args[i].fvarId! let ldecl ← fvarId.getDecl let isNondep : MetaM Bool := args.allM (start := i + 1) λ arg => do diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean index 6de12d8e..7c73ec24 100644 --- a/Aesop/RulePattern.lean +++ b/Aesop/RulePattern.lean @@ -144,7 +144,7 @@ def openRuleType (pat : RulePattern) (inst : RulePatternInstantiation) let mut assigned := ∅ for h : i in [:mvars.size] do if let some inst ← pat.getInstantiation inst i then - let mvarId := mvars[i]'h.2 |>.mvarId! + let mvarId := mvars[i] |>.mvarId! -- We use `isDefEq` to make sure that universe metavariables occurring in -- the type of `mvarId` are assigned. if ← isDefEq (.mvar mvarId) inst then @@ -163,7 +163,7 @@ def specializeRule (pat : RulePattern) (inst : RulePatternInstantiation) if let some inst ← pat.getInstantiation inst i then args := args.push $ some inst else - let fvarId := fvarIds[i]'h.2 + let fvarId := fvarIds[i] args := args.push $ some fvarId remainingFVarIds := remainingFVarIds.push fvarId let result ← mkLambdaFVars remainingFVarIds (← mkAppOptM' rule args) @@ -207,7 +207,7 @@ where let e := s.lctx.mkLambda s.fvars e let mut mvarIdToPos := ∅ for h : i in [:s.fvars.size] do - let name := s.lctx.get! (s.fvars[i]'h.2).fvarId! |>.userName + let name := s.lctx.get! (s.fvars[i]).fvarId! |>.userName mvarIdToPos := mvarIdToPos.insert ⟨name⟩ i let result := { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 5c7cfc4c..fd18c6f3 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -33,7 +33,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern) let mut instMVars := Array.mkEmpty argMVars.size let mut immediateMVars := Array.mkEmpty argMVars.size for h : i in [:argMVars.size] do - let mvarId := argMVars[i]'h.2 |>.mvarId! + let mvarId := argMVars[i].mvarId! if patInstantiatedMVars.contains mvarId then continue if immediate.contains i then diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index dbbafb8a..751c7da9 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -60,7 +60,7 @@ def DynStructureM.run (x : DynStructureM α) (script : UScript) : MetaM (α × Bool) := do let mut steps : PHashMap MVarId (Nat × Step) := {} for h : i in [:script.size] do - let step := script[i]'h.2 + let step := script[i] steps := steps.insert step.preGoal (i, step) let (a, s) ← ReaderT.run x { steps } |>.run {} return (a, s.perfect) diff --git a/Aesop/Script/StructureStatic.lean b/Aesop/Script/StructureStatic.lean index ccfca1b0..b111ce10 100644 --- a/Aesop/Script/StructureStatic.lean +++ b/Aesop/Script/StructureStatic.lean @@ -22,7 +22,7 @@ protected def StaticStructureM.run (script : UScript) (x : StaticStructureM α) CoreM (α × Bool) := do let mut steps : Std.HashMap MVarId (Nat × Step) := Std.HashMap.empty script.size for h : i in [:script.size] do - let step := script[i]'h.2 + let step := script[i] if h : step.postGoals.size = 1 then if step.postGoals[0].goal == step.preGoal then continue diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean index 057e8bec..56866848 100644 --- a/Aesop/Script/Util.lean +++ b/Aesop/Script/Util.lean @@ -18,7 +18,7 @@ def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β) (stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do let mut firstStep? := none for h : pos in [:goals.size] do - let g := goals[pos]'h.2 + let g := goals[pos] if let some step := step? g then if let some (_, _, currentFirstStep) := firstStep? then if stepOrder step < stepOrder currentFirstStep then diff --git a/Aesop/Search/Expansion.lean b/Aesop/Search/Expansion.lean index 729ee123..7b28ff92 100644 --- a/Aesop/Search/Expansion.lean +++ b/Aesop/Search/Expansion.lean @@ -69,7 +69,7 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule) let mut rrefs := Array.mkEmpty rapps.size let mut subgoals := Array.mkEmpty $ rapps.size * 3 for h : i in [:rapps.size] do - let rapp := rapps[i]'h.2 + let rapp := rapps[i] let successProbability := parent.successProbability * (rapp.successProbability?.getD rule.successProbability)