Zulip Chat Archive
Stream: lean4
Topic: Indent after cdot
Patrick Massot (May 06 2023 at 13:37):
Would it be hard to teach the Lean 4 VScode extension to indent when pressing Return at the end of a line starting by · (this is the dot from docs4#Lean.Elab.Tactic.evalTacticCDot)?
Last updated: Dec 20 2023 at 11:08 UTC