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
..
Tactic	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Attr.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Basic.lean	feat: align take/drop/extract across List/Array/Vector (#6860)	2025-01-30 01:24:25 +00:00
Command.lean	feat: parity between structure instance notation and where notation (#6165)	2024-11-30 20:27:25 +00:00
Do.lean	feat: @[builtin_doc] attribute (part 2) (#3918)	2024-09-13 08:05:10 +00:00
Extension.lean	feat: quotations for parser aliases (#4307)	2024-05-30 09:22:22 +00:00
Extra.lean	chore: simplify signature of Array.mapIdx (#5749)	2024-10-21 05:48:42 +00:00
Level.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Module.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
StrInterpolation.lean	feat: @[builtin_doc] attribute (part 2) (#3918)	2024-09-13 08:05:10 +00:00
Syntax.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Tactic.lean	feat: decide +revert and improvements to native_decide (#5999)	2024-11-08 18:17:46 +00:00
Term.lean	fix: typo in partial_fixpoint docstring (#6775)	2025-01-25 14:41:52 +00:00
Types.lean	feat: align take/drop/extract across List/Array/Vector (#6860)	2025-01-30 01:24:25 +00:00