Skip to content

fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions#32989

Open
kim-em wants to merge 10 commits into
leanprover-community:masterfrom
kim-em:simps-respects-non-exposed-body
Open

fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions#32989
kim-em wants to merge 10 commits into
leanprover-community:masterfrom
kim-em:simps-respects-non-exposed-body

Commits

Commits on Apr 17, 2026

Commits on May 27, 2026

Commits on May 28, 2026