Skip to content

experiment: improved 'synthsized type class instance is not definitio…#13814

Draft
TwoFX wants to merge 2 commits into
leanprover:masterfrom
TwoFX:julia/not-equal-error-message
Draft

experiment: improved 'synthsized type class instance is not definitio…#13814
TwoFX wants to merge 2 commits into
leanprover:masterfrom
TwoFX:julia/not-equal-error-message

Commits

Commits on May 22, 2026