Formatter example

format.lean

import Lean

-- The `elab` command is used to define new commands, tactics, and term syntax.
-- We are using it here to define a `#reformat <term>` command that elaborates
-- the given term and then pretty prints it.
open Lean Meta Elab Command Term in
elab "#reformat " s:term : command => liftTermElabM do
  -- `elabTerm` converts `s : Syntax` into an expression `e` without using an expected type (i.e., `none`)
  -- `withSynthesize x` forces pending elaboration problems in `x` to be executed, it applies default instances too.
  let e ← withSynthesize do elabTerm s none
  -- Convert expression `e` into a format object
  let f ← ppExpr e
  -- f.pretty converts format object into a string
  IO.println f.pretty


#reformat fun x   :    Nat => id ( (x+1) )
-- fun x => id (x + 1)

-- Pretty printer has many configuration options, they are all prefixed with `pp.`
set_option pp.funBinderTypes true
#reformat fun x y => (x+1)+y
-- fun (x y : Nat) => x + 1 + y