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
d7d61bfb55
feat: use withoutPosition consistently (part 2)
2022-10-24 12:51:32 -07:00
Leonardo de Moura
562af50191
feat: add ForIn' instance for Range
2022-04-02 18:22:21 -07:00
Sebastian Ullrich
bbfcb1cfb2
perf: allocation-free for i in [n:m] do
2022-01-03 07:03:56 -08:00
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Leonardo de Moura
228bc2dd54
refactor: Traversable => ForM
2021-03-02 06:22:22 -08:00
Leonardo de Moura
35e1f5ad97
refactor: Foldable => Traversable
2021-02-28 16:11:20 -08:00
Leonardo de Moura
ef4d5950ae
feat: add Foldable typeclass
...
We use it in the "`do` unchained" paper.
It will eventually replace `ForIn`.
2021-02-28 09:00:52 -08:00
Leonardo de Moura
5662e2e745
refactor: move ToString Syntax and BEq Syntax to Init
2021-02-26 13:21:04 -08:00
Leonardo de Moura
aae8a35150
feat: add ForIn type class
2021-02-04 17:59:44 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
8c4ac7ccc1
refactor: rename LeanInit ==> Meta, and reduce dependencies
2020-11-13 16:00:31 -08:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
e53874ce45
chore: move to new frontend
2020-10-23 16:32:44 -07:00
Leonardo de Moura
9204b4cc2f
chore: missing specialize
2020-10-12 12:11:17 -07:00
Leonardo de Moura
eacdb5ff83
feat: add Range notation
2020-10-12 11:50:13 -07:00
