mathlib3
feat(data/W): show finitely branching W types are encodable
#1817

Merged

feat(data/W): show finitely branching W types are encodable #1817

mergify merged 7 commits into leanprover-community:master from avigad:wfin

ChrisHughes24 commented on 2019-12-21

robertylewis commented on 2019-12-21

sgouezel added awaiting-author

cipher1024 assigned

robertylewis 6 years ago

feat(data/equiv,data/fintype): an encodable fintype is equiv to a fin

6756824b

feat(data/W): finitely branching W types are encodable

687166e0

feat(archive/examples/prop_encodable): show a type of propositional f…

4103c56b

avigad force pushed from 098c6e80 to b454347d 6 years ago

fix(data/W): remove unused type class argument

7461115b

avigad force pushed from b454347d to 7461115b 6 years ago

fix(data/equiv): add two docstrings

19e16d23

sgouezel removed awaiting-author

sgouezel added awaiting-review

robertylewis commented on 2020-01-27

robertylewis removed awaiting-review

robertylewis added awaiting-author

bryangingechen commented on 2020-01-29

fix(*): multiple fixes from code review

c4c958a5

robertylewis approved these changes on 2020-01-29

robertylewis removed awaiting-author

robertylewis added ready-to-merge

bryangingechen changed the title ~~feat(data/Wfin): show finitely branching W types are encodable~~ feat(data/W): show finitely branching W types are encodable 6 years ago

Merge branch 'master' into wfin

48cb166f

mergify merged 868333b9 into master 6 years ago

Reviewers

robertylewis

bryangingechen

ChrisHughes24

Assignees

robertylewis

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(data/W): show finitely branching W types are encodable #1817 Merged

feat(data/W): show finitely branching W types are encodable #1817

mathlib3
feat(data/W): show finitely branching W types are encodable
#1817

Merged