diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index e79b854a1e..9aa5494ed5 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -452,7 +452,7 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do -- index 2 is unused. pure <| some (← descend ty 2 delab) else pure <| none - `({ $[$fields, ]* $lastField $[: $ty]? }) + `(FIXME) -- `({ $[$fields, ]* $lastField $[: $ty]? }) @[builtinDelab app.Prod.mk] def delabTuple : Delab := whenPPOption getPPNotation do