5c8ebd8868
This PR modifies `Option.instDecidableEq` and `Option.decidableEqNone` so that the latter can be made into a global instance without causing diamonds. It also adds `Option.decidabeNoneEq`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Option.2EdecidableEqNone/near/527226250). --------- Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Rob Simmons <rob@lean-fro.org>
11 lines
329 B
Text
11 lines
329 B
Text
variable {α : Type u} [DecidableEq α]
|
||
|
||
-- test for instance diamonds
|
||
|
||
example (x : Option α) :
|
||
Option.instDecidableEq x none = Option.decidableEqNone x := by
|
||
with_reducible_and_instances rfl
|
||
|
||
example (x : Option α) :
|
||
Option.instDecidableEq none x = Option.decidableNoneEq x := by
|
||
with_reducible_and_instances rfl
|