frequently API
#2330

Merged

feat(order/filter): more eventually/frequently API #2330

mergify merged 6 commits into master from eventually-api

feat(order/filter): more eventually/frequently API

5ab1c87a

urkud commented on 2020-04-05

sgouezel commented on 2020-04-05

urkud commented on 2020-04-05

Update after review

9a439f0e

PatrickMassot added awaiting-review

sgouezel commented on 2020-04-05

Add simp attribute

71d11286

urkud commented on 2020-04-05

Update src/order/filter/basic.lean

b3a46ae4

Update src/order/filter/basic.lean

34c62fde

sgouezel removed awaiting-review

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-04-05

Merge branch 'master' into eventually-api

ae98270a

mergify merged a2e76391 into master 5 years ago

mergify deleted the eventually-api branch 5 years ago

Reviewers

sgouezel

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone