From 48d5c0d2a613180b7466c6a7bb6eeee4c72036af Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 31 Jul 2021 08:39:07 -0700 Subject: [PATCH] chore: pp.proofs defaults to false --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 3 ++- tests/lean/run/PPTopDownAnalyze.lean | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 2df03f6f2d..fb6aa93d23 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -190,7 +190,7 @@ 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 getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o) def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue @@ -349,6 +349,7 @@ partial def delab : Delab := do try let ty ← Meta.inferType (← getExpr) if ← Meta.isProp ty then + -- TODO: make sure the type is analyzed before this delab let stx ← withType delab if ← getPPOption getPPProofsWithType then return ← ``((_ : $stx)) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 0a451215d7..4c6649dfaa 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -67,6 +67,7 @@ universe u v set_option pp.analyze true set_option pp.analyze.checkInstances true +set_option pp.proofs true #testDelab @Nat.brecOn (fun x => Nat) 0 (fun x ih => x) expecting Nat.brecOn (motive := fun x => Nat) 0 fun x ih => x