mathlib3
refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice`
#1783

Merged

refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice` #1783

mergify merged 5 commits into master from bounds-move

refactor(order/bounds,*): move code around to make `order.bounds` not…

436c38f9

sgouezel commented on 2019-12-05

Move more code to `basic`, rewrite the only remaining proof in `default`

8779267d

Rename

5ee779fa

Add `default.lean`

e8348fbc

sgouezel added ready-to-merge

sgouezel approved these changes on 2019-12-07

Merge branch 'master' into bounds-move

dbdd7da4

mergify merged 04559629 into master 6 years ago

mergify deleted the bounds-move branch 6 years ago

Reviewers

sgouezel

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone