improving Array indexing in for loops

Stream: lean4

[Thomas Murrills]

Often when iterating through for loop via index, you're forced to write either

for i in [:as.size] do
  let a := as[i]!

or

for h : i in [:as.size] do
  let a := (as[i]'h.2)

By adding e.g.

macro_rules
| `(tactic|get_elem_tactic_trivial) => `(tactic|exact Membership.mem.upper ‹_›)

you can get away with

for h : i in [:as.size] do
  let a := as[i]

but the h is unfortunately necessary. It would be nice if it could be replaced with _—or, even better, if it wasn't necessary at all.

Would it be a good or bad idea to use forIn' with an inaccessible hypothesis by default for for i in ... (when possible), so that for h : i in ... wasn't necessary in cases like this? (Would there be any technical obstacles, or any significant costs?)

In the future, it would also be nice to gradually make get_elem_tactic_trivial powerful enough (either in core or std) to avoid using []' or []! in most basic for loops. (This would mean being able to handle things like [:as.size-1] as well, as well as using hypotheses like as.size ≤ bs.size when indexing into bs.)

[Joachim Breitner]

I’ve RFC’ed this at https://github.com/leanprover/lean4/issues/3032