max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Data/Option
History
Rob23oba 5e13f81e30
feat: Option.pfilter and other lemmas (#7774) 
This PR adds `Option.pfilter`, a variant of `Option.filter` and several
lemmas for it and other `Option` functions. These lemmas are split off
from #7400.
2025-04-03 08:30:38 +00:00
..
Attach.lean doc: manual docstring review for smaller namespaces (#7365) 2025-03-13 16:09:37 +00:00
Basic.lean doc: manual docstring review for smaller namespaces (#7365) 2025-03-13 16:09:37 +00:00
BasicAux.lean doc: manual docstring review for smaller namespaces (#7365) 2025-03-13 16:09:37 +00:00
Instances.lean feat: Option.pfilter and other lemmas (#7774) 2025-04-03 08:30:38 +00:00
Lemmas.lean feat: Option.pfilter and other lemmas (#7774) 2025-04-03 08:30:38 +00:00
List.lean feat: tree map data structures and operations (#6914) 2025-02-11 14:47:47 +00:00
Monadic.lean feat: mark forIn_pure_yield lemmas simp (#7433) 2025-03-14 00:28:23 +00:00