Skip to content

Commit b1ec186

Browse files
nomeataalgebraic-dev
authored andcommitted
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 245d804 commit b1ec186

File tree

6 files changed

+269
-289
lines changed

6 files changed

+269
-289
lines changed

0 commit comments

Comments
 (0)