mathlib
6df59d68 - feat(data/list/basic): nth_le_enum (#15139)

Commit
3 years ago
feat(data/list/basic): nth_le_enum (#15139) Fill out some of the `enum` and `enum_from` API Link the two via `map_fst_add_enum_eq_enum_from`. Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Author
Parents
Loading