Def Option.maybe.{u,

Modification history

2023-12-21 16:16
Mathlib/Data/Option/Defs.lean
fix(Data/Option/Defs): Remove `Option.rel` and `Option.maybe`, superceded by std4 (#9178) …
Deleted Option.maybe.{u,View on Github →
2021-12-18 19:21
Mathlib/Data/Option/Defs.lean
feat: porting Data.List.Defs, Init.Data.List.Basic (#137) …
Added Option.maybe.{u,View on Github →