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

fix(library/init/lean/expander): mk_notation_transformer: reverse substitution list

Browse source
This commit is contained in:
Sebastian Ullrich 2018-11-23 17:36:34 +01:00
parent ee9c26947c
commit 89b67a0367
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/expander.lean
View file

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