feat: elaborate a[i]! and a[i]?

src/Lean/Elab/App.lean

@@ -900,6 +900,8 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($(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
@@ -1032,6 +1034,8 @@ 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

tests/lean/run/getOp.lean

@@ -0,0 +1,22 @@
+def MyArray := Array
+
+namespace MyArray
+
+def getOp? (self : MyArray α) (idx : Nat) : Option α :=
+  Array.get? self idx
+
+def getOp! [Inhabited α] (self : MyArray α) (idx : Nat) : α :=
+  Array.get! self idx
+
+def getOp (self : MyArray α) (idx : Fin self.size) : α :=
+  Array.get self idx
+
+end MyArray
+
+variable (a : MyArray Nat)
+
+#check a[0]!
+#check a[0]?
+
+variable (i : Fin a.size)
+#check a[i]