Commit 2020-03-07 21:37 d53bbb6e
View on Github →feat(data/fin_enum): fin_enum class for finite types with an enumeration order (#1368)
- feat(data/enum):
enumerableclass for finite types with an enumeration order - little fixes
- Update enum.lean
- Update enum.lean
- Update finset.lean
- add documentation
- Update src/data/enum.lean Co-Authored-By: Scott Morrison scott@tqft.net
- Update src/data/enum.lean [skip ci] Co-Authored-By: Scott Morrison scott@tqft.net
- Update fin.lean [skip ci[
- Update enum.lean
- Update enum.lean
- Update fin.lean [skip ci]
- Update enum.lean
- Update src/data/enum.lean [skip ci] Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
- Update interactive.lean [skip ci]
- Rename enum.lean to fin_enum.lean [skip ci]
- add
mono usingto doc/tactics.md [skip ci] - update to Lean 3.5.1
- address lint comments
- Update src/data/fin_enum.lean Co-Authored-By: Scott Morrison scott@tqft.net
- Update fin_enum.lean
- Apply suggestions from code review Co-Authored-By: Scott Morrison scott@tqft.net
- remove unneeded lemmas
- add
nodup_to_list