r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: Sanitize Syntax

main
Henrik Böving 2021-12-17 23:53:06 +01:00
parent 3c01cf1e68
commit 4380fe088d
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
DocGen4/Process.lean
View File

@ -86,6 +86,7 @@ structure Module where
def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do
let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr)
let (stx, info) ← delabCore Name.anonymous [] expr let (stx, info) ← delabCore Name.anonymous [] expr
let stx := sanitizeSyntax stx |>.run' { options := ←getOptions }
(←parenthesizeTerm stx, info) (←parenthesizeTerm stx, info)
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do