From b89a389427068e6ac25fbad50bfa6f885fca78da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Jul 2019 14:49:40 -0700 Subject: [PATCH] chore(library/init/lean/parser/parser): force eta-expansion --- library/init/lean/parser/parser.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index fa5f263be2..8fe8f0e244 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -237,7 +237,9 @@ instance hashAndthen {k : ParserKind} : HasAndthen (Parser k) := @[inline] def node {k : ParserKind} (n : SyntaxNodeKind) (p : Parser k) : Parser k := { info := nodeInfo p.info, - fn := nodeFn n p.fn } + /- Remark: the compiler currently does not eta-expand structure fields. + So, we force it here to trigger inlining at `node` combinators. -/ + fn := fun a c s => nodeFn n p.fn a c s} @[inline] def leadingNode (n : SyntaxNodeKind) (p : Parser leading) : Parser := node n p