Commit graph

5 commits

Author SHA1 Message Date
Joachim Breitner
684f32fabe
feat: let get_elem_tactic_trivial handle [a]'h.2 (#3132)
The pattern
```
    for h : i in [:xs.size] do
      let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
    for h : i in [:xs.size] do
      let x := xs[i]
```

fixes #3032.
2024-01-08 16:23:09 +00:00
Mario Carneiro
b922483ebc chore: remove getElem' delab 2022-09-21 06:21:00 -07:00
Mario Carneiro
20937c3a6c fix: fix test 2022-09-21 06:21:00 -07:00
Leonardo de Moura
35018dbea2 feat: unexpanders for a[i], a[i]' h, a[i]!, and a[i]? 2022-07-10 06:47:23 -07:00
Leonardo de Moura
881589fc46 chore: remove parser workarounds 2022-07-09 16:42:39 -07:00