diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 9defcfc226..9b50d7252e 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -254,7 +254,7 @@ def numIndices (lctx : LocalContext) : Nat :=
   lctx.decls.size
 
 @[export lean_local_ctx_get]
-def getAt! (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
+def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
   lctx.decls.get! i
 
 section
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index f961def709..900988a1f3 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -289,7 +289,7 @@ where
       let start := lctx.getFVar! xs[0] |>.index
       let stop  := lctx.getFVar! xs.back |>.index
       for i in [start+1:stop] do
-        match lctx.getAt! i with
+        match lctx.getAt? i with
         | some localDecl =>
           if localDecl.isLet then
             return true
@@ -331,7 +331,7 @@ where
       if i+1 == (← read) then
         return ()
       else
-        match (← getLCtx).getAt! (i+1) with
+        match (← getLCtx).getAt? (i+1) with
         | none => collectLetDepsAux i
         | some localDecl =>
           if (← get).contains localDecl.fvarId then
@@ -360,7 +360,7 @@ where
     let stop  := lctx.getFVar! xs.back |>.index
     let mut ys := #[]
     for i in [start:stop+1] do
-      match lctx.getAt! i with
+      match lctx.getAt? i with
       | none => pure ()
       | some localDecl =>
         if s.contains localDecl.fvarId then