Skip to content

feat: warn when simp theorem LHS has variable or unrecognized head symbol#13325

Open
wkrozowski wants to merge 6 commits intoleanprover:masterfrom
wkrozowski:wojciech/simpVarHead2
Open

feat: warn when simp theorem LHS has variable or unrecognized head symbol#13325
wkrozowski wants to merge 6 commits intoleanprover:masterfrom
wkrozowski:wojciech/simpVarHead2

Commits

Commits on Apr 9, 2026