experiment: always check types for instance metavariables at instance…#13846

Draft

TwoFX wants to merge 28 commits into

leanprover:defeq_todo_4_paulfrom

TwoFX:julia/just-try-2

Commits on May 12, 2026

chore: add implicit_reducible/expose attributes to preparatory definitions

authored and
datokrat
committed
test: update tests for defeq changes

authored and
datokrat
committed
chore: add implicit_reducible/expose attributes to library definitions

authored and
datokrat
committed
feat: enable `backward.isDefEq.respectTransparency.types` by default

authored and
datokrat
committed
test: update tests for defeq changes

authored and
datokrat
committed
fix: add `Option.map_some` to `modify_eq_alter` simp sets

authored and
datokrat
committed
fix: remove @[expose] when unnecessary, fixing stage2 warnings in #13823 (#13584)
datokrat
committed
fix errors from rebasing
datokrat
committed
remove respectTransparency.types false

TwoFX
authored and
datokrat
committed
remove local attributes
datokrat
committed
cleanup
datokrat
committed
dsimproc test
datokrat
committed
snapshot
datokrat
committed
Revert "snapshot"
datokrat
committed
remove test files; I gave up trying to satisfy the dsimprocs for now
datokrat
committed
Revert "remove test files; I gave up trying to satisfy the dsimprocs for now"
datokrat
committed
implicit -> instance
datokrat
committed
Reapply "snapshot"
datokrat
committed
poke
datokrat
committed
it compiles
datokrat
committed

Commits on May 16, 2026

linter
datokrat
committed

Commits on May 23, 2026

make Not implicit_reducible
datokrat
committed

Commits on May 26, 2026

Commits on May 27, 2026