lean4

mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

Kim Morrison 5b1c6b558a feat: align take/drop/extract across List/Array/Vector (#6860 )

This PR makes `take`/`drop`/`extract` available for each of
`List`/`Array`/`Vector`. The simp normal forms differ, however: in
`List`, we simplify `extract` to `take+drop`, while in `Array` and
`Vector` we simplify `take` and `drop` to `extract`. We also provide
`Array/Vector.shrink`, which simplifies to `take`, but is implemented by
repeatedly popping. Verification lemmas for `Array/Vector.extract` to
follow in a subsequent PR.

2025-01-30 01:24:25 +00:00

filemap.lean

chore(tests/playground/parser): missing files and small issues

2019-04-12 07:29:46 -07:00

Makefile

test(tests/playground/parser): minor

2019-04-12 09:05:22 -07:00

parser.lean

feat: align take/drop/extract across List/Array/Vector (#6860 )

2025-01-30 01:24:25 +00:00

relative.py

test(tests/playground/parser): create directory and Makefile for experiment