lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

feat: include `ppLine` in `many(1)Indent`

Open tydeu opened this issue 1 year ago • 6 comments

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.

tydeu avatar Aug 23 '23 22:08 tydeu