lean4-htt/src/Init/Data/Option
Kim Morrison face4cef75
feat: complete API for List.replicate (#4487)
This is not the most exciting place to start, but I started here to:
* pick a function with little development in Batteries and Mathlib, so I
wouldn't have conflicts
* that is easy!
* to see how much effort it is to get fairly complete coverage
* and to set up some infrastructure to be used later, i.e.
`tests/lean/run/list_simp.lean`
2024-06-18 08:30:09 +00:00
..
Basic.lean chore: add dates to @[deprecated] attributes (#3967) 2024-05-14 03:24:57 +00:00
BasicAux.lean chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Instances.lean feat: complete API for List.replicate (#4487) 2024-06-18 08:30:09 +00:00
Lemmas.lean chore: remove @[simp] from bind_eq_some (#4314) 2024-06-01 16:04:02 +00:00