From 045fe4ad252a76a1939ce60e7fc8abbb2c55454b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Mar 2017 07:41:42 -0800 Subject: [PATCH] fix(frontends/lean/structure_cmd): allow default values for function fields --- src/frontends/lean/structure_cmd.cpp | 3 ++- tests/lean/run/fn_default.lean | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/fn_default.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 7698261a6b..ec703429be 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -895,7 +895,8 @@ struct structure_cmd_fn { /* TODO(Leo): add helper function for adding definition. It should unfold_untrusted_macros */ expr decl_type = unfold_untrusted_macros(m_env, Pi(args, mlocal_type(field.first))); - expr decl_value = unfold_untrusted_macros(m_env, Fun(args, *field.second)); + expr val = mk_app(m_ctx, get_id_name(), *field.second); + expr decl_value = unfold_untrusted_macros(m_env, Fun(args, val)); name_set used_univs; used_univs = collect_univ_params(decl_value, used_univs); used_univs = collect_univ_params(decl_type, used_univs); diff --git a/tests/lean/run/fn_default.lean b/tests/lean/run/fn_default.lean new file mode 100644 index 0000000000..ec61be1831 --- /dev/null +++ b/tests/lean/run/fn_default.lean @@ -0,0 +1,6 @@ +structure foo := +(bar : Π n : ℕ, ℕ := id) +(baz : Π {n : ℕ}, ℕ := id) +(bat : Π n : ℕ, ℕ := λ n, n) + +check {foo.}