more

leanprover-community · Dec 15, 2024 · f6befd9 · f6befd9
1 parent 7008f8a
commit f6befd9
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git 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/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
@@ -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
@@ -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/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)