Skip to content

fix: keep the space before a hygieneInfo antiquotation - #15025

Open
mhuisi wants to merge 1 commit into
leanprover:masterfrom
mhuisi:push-vnppputzlnsn
Open

fix: keep the space before a hygieneInfo antiquotation#15025
mhuisi wants to merge 1 commit into
leanprover:masterfrom
mhuisi:push-vnppputzlnsn

Commits

Commits on Sep 4, 2026