From 2ef84a1b64ccb9fcfeb8a7d5cf689bf3dc796cd2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2020 16:03:40 -0800 Subject: [PATCH] chore: temporary staging workaround @Kha It seems the new builtin antiquotation notation you added depends on the array literal notation that is not builtin. I got the following error after `update-stage0` ``` Lean/PrettyPrinter/Delaborator/Builtins.lean:455:2: error: elaboration function for '_kind.term._@.Init.Data.Array.Basic._hyg.3391' has not been implemented ``` The base name changed from `_kind.term` to `termKind`. I had to change it because every parser we were defining was in the artificial (sub-)namespace `_kind` :) We didn't notive because we didn't have scoped parsers. --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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