fix: respect transparency#13342

Draft

datokrat wants to merge 18 commits intodefeq_todo_4from

defeq_todo_4_paul

Commits on Apr 7, 2026

chore: add implicit_reducible/expose attributes to preparatory definitions

authored and
kim-em
committed
test: update tests for defeq changes

authored and
kim-em
committed
chore: add implicit_reducible/expose attributes to library definitions

authored and
kim-em
committed
feat: enable `backward.isDefEq.respectTransparency.types` by default

authored and
kim-em
committed
test: update tests for defeq changes

authored and
kim-em
committed

Commits on Apr 8, 2026

Julias changes

TwoFX
authored and
datokrat
committed
progress
datokrat
committed

Commits on Apr 9, 2026

Commits on Apr 10, 2026

-m
datokrat
committed
fix slice.lean by un-@[rfl]'in
datokrat
committed
systematic fix 1

hargoniX
authored and
datokrat
committed
dsimp to simp

hargoniX
authored and
datokrat
committed
change cast

hargoniX
authored and
datokrat
committed
more simp

hargoniX
authored and
datokrat
committed
fix lrat checker

hargoniX
authored and
datokrat
committed
flat order quickfix
datokrat
committed
remove log entries
datokrat
committed