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 23925f2 commit 5b25c4eCopy full SHA for 5b25c4e
1 file changed
MathlibTest/ToDual.lean
@@ -32,7 +32,6 @@ structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α
32
attribute [to_dual existing] Lattice.toSemilatticeInf
33
34
-- we can reorder arguments of arguments in `SemilatticeInf.mk`
35
-set_option linter.impossibleInstance false in
36
@[to_dual, reducible]
37
def le_inf_test [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
38
le_inf
0 commit comments