Skip to content

fix: add expected type hints to Sym rules modified by preprocessing - #16140

Open
kmehltretter82 wants to merge 3 commits into
leanprover:masterfrom
kmehltretter82:fix-sym-thm-expected-prop-hint
Open

fix: add expected type hints to Sym rules modified by preprocessing#16140
kmehltretter82 wants to merge 3 commits into
leanprover:masterfrom
kmehltretter82:fix-sym-thm-expected-prop-hint

fix: restrict Sym backward rule hints to proofs

4b24d09
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 error, 1 warning, and 1 notice
check-pr-body
failed Nov 7, 2026 in 4s