Skip to content

[#14537] spike: better defeq error messages - #17

Draft
downstream-lean4[bot] wants to merge 2 commits into
masterfrom
adaptation-14537
Draft

[#14537] spike: better defeq error messages#17
downstream-lean4[bot] wants to merge 2 commits into
masterfrom
adaptation-14537

Commits

Commits on Jul 24, 2026