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

feat: pp.analyze default transparency

Browse source
This commit is contained in:
Daniel Selsam 2021-07-31 18:45:33 -07:00 • committed by Sebastian Ullrich
parent aefd31b2a2
commit be02133ca7
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
View file

@ -192,8 +192,7 @@ def isDefEqAssigning (t s : Expr) : MetaM Bool := do
def checkpointDefEq (t s : Expr) : MetaM Bool := do
Meta.checkpointDefEq (mayPostpone := false) do
withTransparency TransparencyMode.instances do
isDefEqAssigning t s
isDefEqAssigning t s
def tryUnify (t s : Expr) : MetaM Unit := do
try