From c325438453a2fee8dd0217e902d4eaed0a1d90c8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 14 Mar 2017 14:40:22 +0100 Subject: [PATCH] fix(frontends/lean/elaborator): let expr patterns --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e5248b115f..6d8963682b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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))