Skip to content

Commit d60ef53

Browse files
authored
refactor: make CCPO class Prop-valued (#11425)
This PR changes `Lean.Order.CCPO` and `.CompleteLattice` to carry a Prop. This avoids the `CCPO IO` instance from being `noncomputable`.
1 parent dd57725 commit d60ef53

File tree

6 files changed

+269
-289
lines changed

6 files changed

+269
-289
lines changed

0 commit comments

Comments
 (0)