feat: allow decidable equality for empty lists and empty arrays#11269

Merged

robsimmons merged 11 commits intomasterfrom

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
Make arrays have empty deceq, even though they're not yet definitonally equal
robsimmons
committed

Commits on Nov 20, 2025