feat: parenthesize in the pretty printer
parent
8c30f29542
commit
ac8d9e254e
|
@ -72,8 +72,9 @@ structure Module where
|
||||||
members : Array DocInfo
|
members : Array DocInfo
|
||||||
deriving Inhabited
|
deriving Inhabited
|
||||||
|
|
||||||
def prettyPrintTerm (expr : Expr) : MetaM Syntax :=
|
def prettyPrintTerm (expr : Expr) : MetaM Syntax := do
|
||||||
delab Name.anonymous [] expr
|
let term ← delab Name.anonymous [] expr
|
||||||
|
parenthesizeTerm term
|
||||||
|
|
||||||
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
|
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
|
||||||
let env ← getEnv
|
let env ← getEnv
|
||||||
|
|
Loading…
Reference in New Issue