feat: make `Option.decidableEqNone` coherent with `Option.instDecidableEq`#9302

Merged

robsimmons merged 7 commits intoleanprover:masterfrom

plp127:aliu/option

Nov 20, 2025

Commits on Nov 19, 2025

modify instances

plp127
authored and
robsimmons
committed
add tests

plp127
authored and
robsimmons
committed
rename test

plp127
authored and
robsimmons
committed
Update src/Init/Data/Option/Basic.lean

authored and
robsimmons
committed
try to fix tests

plp127
authored and
robsimmons
committed
move instances

plp127
authored and
robsimmons
committed
Remove duplication from merge
robsimmons
committed