chore: remove parser workarounds

src/Init/Tactics.lean

@@ -434,8 +434,12 @@ macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| decide)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| assumption)
 
-macro "get_elem_tactic" : tactic => `(get_elem_tactic_trivial) -- TODO: add error message
+macro "get_elem_tactic" : tactic =>
+  `(first
+    | get_elem_tactic_trivial
+    | fail "failed to prove index is valid, possible solutions:\n  - Use `have`-expressions to prove the index is valid\n  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid\n  - Use `a[i]?` notation instead, result is an `Option` type\n  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
+   )
 
-macro:max (priority := high) x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
+macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
 
 macro x:term noWs "[" i:term "]'" h:term:max : term => `(getElem $x $i $h)

src/Init/Util.lean

@@ -59,10 +59,10 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
 @[inline] def getElem! [GetElem Cont Idx Elem Dom] [Inhabited Elem] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Elem :=
-  if h : _ then getElem xs i h else unreachable!
+  if h : _ then getElem xs i h else panic! "index out of bounds"
 
 @[inline] def getElem? [GetElem Cont Idx Elem Dom] (xs : Cont) (i : Idx) [Decidable (Dom xs i)] : Option Elem :=
   if h : _ then some (getElem xs i h) else none
 
-macro:max (priority := high) x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i) -- TODO: remove priority
-macro:max (priority := high) x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i) -- TODO: remove priority
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)

tests/lean/getElem.lean

@@ -0,0 +1,22 @@
+def f1 (a : Array Nat) (i : Nat) :=
+  a[i]
+
+def f2 (a : Array Nat) (i : Fin a.size) :=
+  a[i] -- Ok
+
+def f3 (a : Array Nat) (h : n ≤ a.size) (i : Fin n) :=
+  a[i] -- Ok
+
+opaque a : Array Nat
+opaque n : Nat
+axiom n_lt_a_size : n < a.size
+
+def f4 (i : Nat) (h : i < n) :=
+  have : i < a.size := Nat.lt_trans h n_lt_a_size
+  a[i]
+
+def f5 (i : Nat) (h : i < n) :=
+  a[i]'(Nat.lt_trans h n_lt_a_size)
+
+def f6 (i : Nat) :=
+  a[i]!

tests/lean/getElem.lean.expected.out

@@ -0,0 +1,8 @@
+getElem.lean:2:2-2:6: error: failed to prove index is valid, possible solutions:
+  - Use `have`-expressions to prove the index is valid
+  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
+  - Use `a[i]?` notation instead, result is an `Option` type
+  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
+a : Array Nat
+i : Nat
+⊢ i < Array.size a