mathlib3
chore(order/filter): rephrase filter.has_le
#1399
Merged

chore(order/filter): rephrase filter.has_le #1399

mergify merged 2 commits into master from filter-order-tweak
PatrickMassot
chore(order/filter): rephrase filter.has_le
85fd317a
PatrickMassot PatrickMassot requested a review 6 years ago
PatrickMassot PatrickMassot assigned sgouezel sgouezel 6 years ago
sgouezel
sgouezel approved these changes on 2019-09-05
sgouezel sgouezel added ready-to-merge
mergify[bot] Merge branch 'master' into filter-order-tweak
3b9081f8
mergify mergify merged 7f208430 into master 6 years ago
mergify mergify deleted the filter-order-tweak branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone