fixes

leanprover-community · Nov 12, 2024 · 4092e80 · 4092e80
1 parent 6d7410d
commit 4092e80
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean
@@ -50,7 +50,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern)
         (proofTypesAcc : Std.HashSet Expr) :
         MetaM (Array (Expr × Nat) × Array FVarId × Std.HashSet Expr) := do
       if h : i < immediateMVars.size then
-        let mvarId := immediateMVars.get ⟨i, h⟩
+        let mvarId := immediateMVars[i]
         let type ← mvarId.getType
         (← getLCtx).foldlM (init := (proofsAcc, usedHypsAcc, proofTypesAcc)) λ s@(proofsAcc, usedHypsAcc, proofTypesAcc) ldecl => do
           if ldecl.isImplementationDetail then

diff --git a/Aesop/Tree/TreeM.lean b/Aesop/Tree/TreeM.lean
@@ -92,7 +92,7 @@ def getRootGoal : TreeM GoalRef := do
   let cref ← getRootMVarCluster
   let grefs := (← cref.get).goals
   if h : grefs.size = 1 then
-    return grefs.get ⟨0, by simp [h]⟩
+    return grefs[0]
   else
     throwError "aesop: internal error: unexpected number of goals in root mvar cluster: {grefs.size}"