Skip to content

Commit 3c4fc1f

Browse files
cppioalgebraic-dev
authored andcommitted
chore: add missing instance (leanprover#8772)
Changes `ReverseImplicationOrder.instCompleteLattice` to be an `instance`.
1 parent 17f5cc6 commit 3c4fc1f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Internal/Order/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -914,7 +914,7 @@ instance ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrde
914914
rel_antisymm h₁ h₂ := propext ⟨h₂, h₁⟩
915915

916916
-- This defines a complete lattice on `Prop`, used to define coinductive predicates
917-
def ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
917+
instance ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
918918
sup c := ∀ p, c p → p
919919
sup_spec := by
920920
intro x c

0 commit comments

Comments
 (0)