mathlib3
feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order
#1368
Merged
Overview
Commits
25
Changes
View On GitHub

feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order #1368

mergify merged 25 commits into master from enumerable
cipher1024
cipher1024 cipher1024 requested a review 6 years ago
kim-em
kim-em commented on 2019-08-30
kim-em
kim-em commented on 2019-08-30
kim-em
kim-em commented on 2019-08-30
kim-em
cipher1024
rwbarton
rwbarton commented on 2019-09-04
cipher1024 cipher1024 assigned rwbarton rwbarton 6 years ago
robertylewis
robertylewis robertylewis added needs-documentation
cipher1024 cipher1024 force pushed from e1b194db to ddbab4a6 6 years ago
kim-em
kim-em requested changes on 2019-09-23
cipher1024
cipher1024 cipher1024 requested a review from rwbarton rwbarton 6 years ago
bryangingechen
bryangingechen commented on 2019-11-16
bryangingechen
bryangingechen commented on 2019-11-16
bryangingechen bryangingechen changed the title feat(data/enum): `enumerable` class for finite types with an enumeration order feat(data/enum): `fin_enum` class for finite types with an enumeration order 6 years ago
bryangingechen
bryangingechen bryangingechen changed the title feat(data/enum): `fin_enum` class for finite types with an enumeration order feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order 6 years ago
bryangingechen bryangingechen removed needs-documentation
bryangingechen bryangingechen added awaiting-review
kim-em
kim-em
kim-em dismissed these changes on 2020-02-20
kim-em kim-em dismissed their stale review 6 years ago
oops
cipher1024 feat(data/enum): `enumerable` class for finite types with an
672de93b
cipher1024 little fixes
be74d7c6
cipher1024 Update enum.lean
17687580
cipher1024 Update enum.lean
674912da
cipher1024 Update finset.lean
9c6dd4c5
cipher1024 add documentation
dcd05fce
cipher1024 Update src/data/enum.lean
99890d12
cipher1024 Update src/data/enum.lean [skip ci]
1ce5a8f3
cipher1024 Update fin.lean [skip ci[
e51cb780
cipher1024 Update enum.lean
eb7c556a
cipher1024 Update enum.lean
23551fd2
cipher1024 Update fin.lean [skip ci]
a1f95251
cipher1024 Update enum.lean
37bce663
cipher1024 Update src/data/enum.lean [skip ci]
1f3e663c
cipher1024 Update interactive.lean [skip ci]
7a988f49
cipher1024 Rename enum.lean to fin_enum.lean [skip ci]
0da7e170
bryangingechen add `mono using` to doc/tactics.md [skip ci]
4246f67a
cipher1024 cipher1024 force pushed from 12c3adaf to 48869e0c 6 years ago
cipher1024 update to Lean 3.5.1
bcb53090
cipher1024 cipher1024 force pushed from 48869e0c to bcb53090 6 years ago
cipher1024 address lint comments
ae803764
kim-em
kim-em commented on 2020-02-28
kim-em
kim-em commented on 2020-02-28
kim-em
kim-em commented on 2020-02-28
kim-em
kim-em commented on 2020-02-28
kim-em
kim-em commented on 2020-02-28
kim-em
cipher1024 Update src/data/fin_enum.lean
2214b1ab
cipher1024 Update fin_enum.lean
6c72db9f
cipher1024 Apply suggestions from code review
fe8b9229
cipher1024 remove unneeded lemmas
ce3c02fe
cipher1024 cipher1024 force pushed from 04168b83 to ce3c02fe 6 years ago
kim-em
kim-em commented on 2020-03-03
cipher1024 add `nodup_to_list`
fd0dd8a1
kim-em
kim-em approved these changes on 2020-03-04
kim-em kim-em removed awaiting-review
kim-em kim-em added ready-to-merge
kim-em
kim-em approved these changes on 2020-03-07
mergify[bot] Merge branch 'master' into enumerable
d3ce51c2
mergify mergify merged d53bbb6e into master 6 years ago
mergify mergify deleted the enumerable branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum