From dfc88ef99f7ca331017713dcb5845d0802afb6df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Jul 2022 16:44:52 -0700 Subject: [PATCH] chore: use `a[i]` --- src/Lean/Meta/ExprDefEq.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index eb4c2c7195..15cf0db49b 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -166,7 +166,7 @@ private partial def isDefEqArgsFirstPass (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM (Option (Array Nat)) := do let rec loop (i : Nat) (postponed : Array Nat) := do if h : i < paramInfo.size then - let info := paramInfo.get ⟨i, h⟩ + let info := paramInfo[i] let a₁ := args₁[i]! let a₂ := args₂[i]! if !info.isExplicit then @@ -197,8 +197,9 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let (some postponed) ← isDefEqArgsFirstPass finfo.paramInfo args₁ args₂ | pure false let rec processOtherArgs (i : Nat) : MetaM Bool := do if h₁ : i < args₁.size then - let a₁ := args₁.get ⟨i, h₁⟩ - let a₂ := args₂.get ⟨i, Eq.subst h h₁⟩ + let a₁ := args₁[i] + have : i < args₂.size := h ▸ h₁ + let a₂ := args₂[i] if (← Meta.isExprDefEqAux a₁ a₂) then processOtherArgs (i+1) else