Skip to content

Commit e07ed1a

Browse files
authored
chore: add missing instance (#8772)
Changes `ReverseImplicationOrder.instCompleteLattice` to be an `instance`.
1 parent d247297 commit e07ed1a

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)