basic): redefine `filter.pure`
#1889

Merged

refactor(order/filter/basic): redefine `filter.pure` #1889

mergify merged 8 commits into master from filter-pure-def

refactor(order/filter/basic): redefine `filter.pure`

1769d653

cipher1024 assigned

sgouezel 6 years ago

urkud added awaiting-review

gebner commented on 2020-01-21

Update src/order/filter/basic.lean

f34b438d

sgouezel removed awaiting-review

sgouezel added awaiting-author

Minor fixes suggested by @gebner

fa8066c6

Merge branch 'filter-pure-def' of git://github.com/leanprover-communi…

ff22ea0a

urkud removed awaiting-author

urkud added awaiting-review

Merge branch 'master' into filter-pure-def

348c26c6

Fix compile

f55f2a46

sgouezel commented on 2020-01-26

Update src/order/filter/basic.lean

df7c75ee

sgouezel removed awaiting-review

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-01-26

Merge branch 'master' into filter-pure-def

c49b5b82

mergify merged 587b312e into master 6 years ago

mergify deleted the filter-pure-def branch 6 years ago

Reviewers

sgouezel

gebner

Assignees

sgouezel

Labels

ready-to-merge

Milestone

No milestone