max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/parser/parser): force eta-expansion

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 14:49:40 -07:00
parent 324a053f4c
commit b89a389427
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/parser.lean
View file

@ -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