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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-04 18:11:53 -08:00
parent 42232609b9
commit b37213e378
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -452,7 +452,7 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
-- index 2 is unused.
pure <| some (← descend ty 2 delab)
else pure <| none
`(FIXME) -- `({ $[$fields, ]* $lastField $[: $ty]? })
`({ $[$fields, ]* $lastField $[: $ty]? })
@[builtinDelab app.Prod.mk]
def delabTuple : Delab := whenPPOption getPPNotation do