Markus Himmel
8eec1e4cfb
feat: Option lemmas and cleanup ( #8298 )
...
This PR adds various `Option` lemmas and defines `Option.filterM` for
applicative functors.
2025-05-13 08:42:03 +00:00
Markus Himmel
68d9d14d44
chore: do not use the coercion α → Option α in Init and Std ( #8085 )
...
This PR moves the coercion `α → Option α` to the new file
`Init.Data.Option.Coe`. This file may not be imported anywhere in `Init`
or `Std`.
2025-04-24 13:35:01 +00:00
Sebastian Ullrich
7feb583b9e
feat: enable experimental module system in Init ( #8047 )
2025-04-23 17:21:33 +00:00
Kim Morrison
00c7b85261
feat: lemmas about for loops over Option ( #6316 )
...
This PR adds lemmas simplifying `for` loops over `Option` into
`Option.pelim`, giving parity with lemmas simplifying `for` loops of
`List` into `List.fold`.
2024-12-05 05:09:07 +00:00
Kim Morrison
1fca66b8c9
feat: Option.attach ( #5532 )
2024-09-30 04:13:27 +00:00
Scott Morrison
eaf44d74ae
chore: upstream Option material from Std ( #3356 )
2024-02-16 02:05:18 +00: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
c445199747
chore: library/Init ==> src/Init
...
cc @Kha @dselsam @cipher1024
2019-11-22 06:06:05 -08:00
