We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 86d935e commit 7928507Copy full SHA for 7928507
src/Init/Internal/Order/Basic.lean
@@ -914,7 +914,7 @@ instance ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrde
914
rel_antisymm h₁ h₂ := propext ⟨h₂, h₁⟩
915
916
-- This defines a complete lattice on `Prop`, used to define coinductive predicates
917
-instance ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
+def ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder where
918
sup c := ∀ p, c p → p
919
sup_spec := by
920
intro x c
0 commit comments