lean4
lean4 copied to clipboard
feat: include `ppLine` in `many(1)Indent`
I noticed many1Ident
did not pretty print lines during this Zulip thread. Including ppLine
within manyIdent
will help end users get better pretty printer output without needing initmate knowledge of when to use the pp*
helpers.