Pretty printing

[david-christiansen]

What question should the reference manual answer?

How do I customize pretty-printing for my syntax?

What are the differences between custom delaborators, unexpanders, and formatters? How can they be used?

[fpvandoorn]

I think a diagram containing the following arrows could be useful (similar to the diagram at the start of Ch 2)

delaborator : Expr -> Syntax
unexpander : Syntax -> Syntax
formatter : Syntax -> Format (or MessageData?)

I talked told my students a little bit about printing, with the following example (this depends on Mathlib, but maybe you can do something similar) - although I guess a reference guide doesn't typically explain via examples.

import Mathlib.Algebra.BigOperators.Group.List

open Lean Meta Elab Parser Tactic PrettyPrinter

/- before this I gave some examples with notation, etc. -/

/- You can be even more flexible with *macros*. -/
macro "∑ " x:ident " ∈ " l:term ", " f:term : term => `(List.sum (List.map (fun $x => $f) $l))
#eval ∑ x ∈ [1,2,3], x ^ 3

/- Remark: macros are not automatically pretty-printed. -/
#check ∑ x ∈ [1,2,3], x ^ 3

/- Declaring your own pretty-printer is a bit cumbersome.
Luckily `notation` and similar commands do it for you. -/

@[app_unexpander List.sum]
def unexpListMap : Unexpander
  | `($_ $a) =>
    match a with
    | `(List.map $f $l) =>
      match f with
      | `(fun $x:ident ↦ $f) => `(∑ $x ∈ $l, $f)
      | _ => throw ()
    | _ => throw ()
  | _ => throw ()

#check ∑ x ∈ [1,2,3], x ^ 3

[david-christiansen]

Thanks, this is a good suggestion! A reference should not explain via examples, but including illustrative examples in addition to explicitly writing down the rules is a useful and important thing to do.