Include more information while pretty-printing

[siddhartha-gadgil]

It will be useful to have types for functions and pi-types. Here is some code.

def ppExprDetailed (e : Expr): MetaM Format := do
  let fmtDetailed ← withOptions (fun o₁ =>
                    let o₂ := pp.motives.all.set o₁ true
                    let o₃ := pp.fieldNotation.set o₂ false
                    let o₄ := pp.proofs.set o₃ true
                    let o₅ := pp.deepTerms.set o₄ true
                    let o₆ := pp.funBinderTypes.set o₅ true
                    let o₇ := pp.piBinderTypes.set o₆ true
                    let o₈ := pp.letVarTypes.set o₇ true
                    pp.unicode.fun.set o₈ true) do
    ppExpr e
  return fmtDetailed

One also needs to update databases.

[siddhartha-gadgil]

We also need versions of this for ppCommand.

[siddhartha-gadgil]

This is done, but should be made usable in translate and/or bulkelab