mathlib3
chore(data/set/lattice): use dot syntax for `disjoint.*`
#2282
Merged

chore(data/set/lattice): use dot syntax for `disjoint.*` #2282

mergify merged 2 commits into master from dot-syntax
urkud
urkud chore(data/set/lattice): use dot syntax for `disjoint.*`
b4f2ead7
ChrisHughes24
ChrisHughes24 approved these changes on 2020-03-29
ChrisHughes24 ChrisHughes24 added ready-to-merge
mergify[bot] Merge branch 'master' into dot-syntax
54c51f3d
mergify mergify merged 51553e36 into master 5 years ago
urkud urkud deleted the dot-syntax branch 5 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone