max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: pp option to instantiate mvars

Browse source
This commit is contained in:
Daniel Selsam 2021-07-29 11:23:41 -07:00 • committed by Sebastian Ullrich
parent b3bb82ee7e
commit aa590ccdf5
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/PrettyPrinter/Delaborator/Basic.lean
View file

@ -71,6 +71,11 @@ register_builtin_option pp.binderTypes : Bool := {
group := "pp"
descr := "(pretty printer) display types of lambda and Pi parameters"
}
register_builtin_option pp.instantiateMVars : Bool := {
defValue := false -- TODO: default to true?
group := "pp"
descr := "(pretty printer) instantiate mvars before delaborating"
}
register_builtin_option pp.structureInstances : Bool := {
defValue := true
group := "pp"
@ -183,6 +188,7 @@ def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanc
def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)
def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o || getPPAnalyze o)
def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue
@ -382,6 +388,7 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options
if ← Meta.isProp ty then
opts := pp.proofs.set opts true
catch _ => pure ()
let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e
let optionsPerPos ←
if getPPAnalyze opts && optionsPerPos.isEmpty then
topDownAnalyze e