diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index ba73523eb6..492bd24bc4 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -37,12 +37,17 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do let e โ† whnfCore e if e matches Expr.lam .. then lambdaLetTelescope e fun _ e => parserNodeKind? e - else if e.isAppOfArity ``nodeWithAntiquot 4 || e.isAppOfArity ``withAntiquot 2 || e.isAppOfArity ``withCache 2 then - parserNodeKind? (e.getArg! 1) else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then reduceEval? (e.getArg! 0) - else - return none + else if e.isAppOfArity ``withAntiquot 2 then + parserNodeKind? (e.getArg! 1) + else forallTelescope (โ† inferType e.getAppFn) fun params _ => do + let lctx โ† getLCtx + -- if there is exactly one parameter of type `Parser`, search there + if let [(i, _)] := params.toList.enum.filter (lctx.getFVar! ยท.2 |>.type.isConstOf ``Parser) then + parserNodeKind? (e.getArg! i) + else + return none section open Meta