From 89b67a0367e517f37f914fce1cebc77d524eac4e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 23 Nov 2018 17:36:34 +0100 Subject: [PATCH] fix(library/init/lean/expander): mk_notation_transformer: reverse substitution list --- library/init/lean/expander.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index dd65d62273..e0363cc925 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -57,7 +57,7 @@ structure notation_transformer_state := (stx : syntax) -- children of `stx` that have not been consumed yet (stx_args : list syntax := []) --- substitutions for notation variables +-- substitutions for notation variables (reversed) (substs : list (syntax_ident × syntax) := []) -- filled by `binders` transitions, consumed by `scoped` actions (scoped : option $ term.binders.view := none) @@ -100,6 +100,7 @@ def mk_notation_transformer (nota : notation_macro) : expander.transformer := | none := pure () | _ := error stx "mk_notation_transformer: unimplemented"), st ← get, + let substs := st.substs.reverse, -- apply substitutions [(x1, e1), ...] via `(λ x1 ..., nota.nota.term) e1 ...` let lam := review lambda {binders := st.substs.map prod.fst, body := nota.nota.term}, pure $ some $ st.substs.foldl (λ fn subst, review app {fn := fn, arg := subst.2}) lam