We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent d19b504 commit 671e6c1Copy full SHA for 671e6c1
src/Lean/Elab/Command.lean
@@ -611,7 +611,7 @@ def withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) : Comm
611
finally
612
modify ({ · with nextMacroScope })
613
614
-private partial def recordUsedSyntaxKinds (stx : Syntax) : CommandElabM Unit := do
+private partial def recordUsedSyntaxKinds (stx : Syntax) : CoreM Unit := do
615
if let .node _ k .. := stx then
616
-- do not record builtin parsers, they do not have to be imported
617
if !(← Parser.builtinSyntaxNodeKindSetRef.get).contains k then
0 commit comments