diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 78c0881286..fa41e22eaf 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -665,7 +665,6 @@ inductive LValResolution where
   | projIdx  (structName : Name) (idx : Nat)
   | const    (baseStructName : Name) (structName : Name) (constName : Name)
   | localRec (baseName : Name) (fullName : Name) (fvar : Expr)
-  | getOp    (fullName : Name) (idx : Syntax)
 
 private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
   throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
@@ -762,18 +761,11 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       | none                => searchCtx ()
     else
       searchCtx ()
-  | some structName, LVal.getOp _ idx kind =>
-    let env ← getEnv
-    let fullName := Name.mkStr structName kind.opName
-    match env.find? fullName with
-    | some _ => return LValResolution.getOp fullName idx
-    | none   => throwLValError e eType m!"invalid [..] notation because environment does not contain '{fullName}'"
   | none, LVal.fieldName _ _ (some suffix) _ =>
     if e.isConst then
       throwUnknownConstant (e.constName! ++ suffix)
     else
       throwInvalidFieldNotation e eType
-  | _, LVal.getOp .. => throwInvalidFieldNotation e eType
   | _, _ => throwInvalidFieldNotation e eType
 
 /- whnfCore + implicit consumption.
@@ -929,17 +921,6 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       else
         let f ← elabAppArgs fvar #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
-    | LValResolution.getOp fullName idx =>
-      let getOpFn ← mkConst fullName
-      let getOpFn ← addTermInfo lval.getRef getOpFn
-      if lvals.isEmpty then
-        let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
-        let namedArgs ← addNamedArg namedArgs { name := `idx,  val := Arg.stx idx }
-        elabAppArgs getOpFn namedArgs args expectedType? explicit ellipsis
-      else
-        let f ← elabAppArgs getOpFn #[{ name := `self, val := Arg.expr f }, { name := `idx, val := Arg.stx idx }]
-                            #[] (expectedType? := none) (explicit := false) (ellipsis := false)
-        loop f lvals
   loop f lvals
 
 private def elabAppLVals (f : Expr) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
@@ -1045,9 +1026,6 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
     | `($(e).$field:ident) => elabFieldName e field
     | `($e |>.$field:ident) => elabFieldName e field
-    | `($e[%$bracket $idx]) => elabAppFn e (LVal.getOp bracket idx .safe :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `($e[%$bracket $idx]!) => elabAppFn e (LVal.getOp bracket idx .panic :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `($e[%$bracket $idx]?) => elabAppFn e (LVal.getOp bracket idx .optional :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     | `($_:ident@$_:term) =>
       throwError "unexpected occurrence of named pattern"
     | `($id:ident) => do
@@ -1179,9 +1157,6 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtinTermElab choice] def elabChoice : TermElab := elabAtom
 @[builtinTermElab proj] def elabProj : TermElab := elabAtom
-@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
-@[builtinTermElab arrayRefOpt] def elabArrayRefOpt : TermElab := elabAtom
-@[builtinTermElab arrayRefPanic] def elabArrayRefPanic : TermElab := elabAtom
 
 builtin_initialize
   registerTraceClass `Elab.app
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 7c7819d461..57d5bc3796 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -372,16 +372,6 @@ opaque mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab)
 
 builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute
 
-inductive GetOpKind where
-  | /-- `a[i]` -/  safe
-  | /-- `a[i]!` -/ panic
-  | /-- `a[i]?` -/ optional
-
-def GetOpKind.opName : GetOpKind → String
-  | safe => "getOp"
-  | panic => "getOp!"
-  | optional => "getOp?"
-
 /--
   Auxiliary datatatype for presenting a Lean lvalue modifier.
   We represent a unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
@@ -393,12 +383,10 @@ inductive LVal where
     /- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.
        `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
   | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
-  | getOp     (ref : Syntax) (idx : Syntax) (getOpKind : GetOpKind)
 
 def LVal.getRef : LVal → Syntax
   | LVal.fieldIdx ref _    => ref
   | LVal.fieldName ref ..  => ref
-  | LVal.getOp ref ..      => ref
 
 def LVal.isFieldName : LVal → Bool
   | LVal.fieldName .. => true
@@ -408,12 +396,6 @@ instance : ToString LVal where
   toString
     | LVal.fieldIdx _ i     => toString i
     | LVal.fieldName _ n .. => n
-    | LVal.getOp _ idx k    =>
-      let r := "[" ++ toString idx ++ "]"
-      match k with
-      | .safe => r
-      | .panic => r ++ "!"
-      | .optional => r ++ "?"
 
 /-- Return the name of the declaration being elaborated if available. -/
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 75130c3146..29ff0373ce 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -266,9 +266,6 @@ def argument       :=
 
 @[builtinTermParser] def proj     := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
 @[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
-@[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
-@[builtinTermParser] def arrayRefOpt := trailing_parser checkNoWsBefore >> "[" >> termParser >> "]" >> checkNoWsBefore >> "?"
-@[builtinTermParser] def arrayRefPanic := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]" >> checkNoWsBefore >> "!"
 @[builtinTermParser] def arrow    := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
 
 def isIdent (stx : Syntax) : Bool :=