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

fix(frontends/lean/elaborator): let expr patterns

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-14 14:40:22 +01:00 • committed by Leonardo de Moura
parent 647d7a8501
commit c325438453
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -2705,7 +2705,7 @@ static expr quote(expr const & e) {
return mk_app(mk_constant({"expr", "pi"}), mk_expr_placeholder(), mk_expr_placeholder(),
quote(binding_domain(e)), quote(binding_body(e)));
case expr_kind::Let:
return mk_app(mk_constant({"expr", "let"}), mk_expr_placeholder(), quote(let_type(e)),
return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
quote(let_value(e)), quote(let_body(e)));
case expr_kind::Macro:
if (is_antiquote(e))