From c4ebfab14c6583995bef0f99f5196765331d5569 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 6 Mar 2017 13:14:10 +0100 Subject: [PATCH] fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter --- src/frontends/lean/structure_cmd.cpp | 2 +- tests/lean/run/struct_bug3.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/struct_bug3.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index b78961cbd8..c340ffd192 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -466,7 +466,7 @@ struct structure_cmd_fn { return ::lean::mk_field_default_value(m_env, full_field_name, [&](name const & fname) { for (field_decl const & d : m_fields) { if (local_pp_name(d.first) == fname) - return some_expr(d.first); + return some_expr(mk_explicit(d.first)); } return none_expr(); }); diff --git a/tests/lean/run/struct_bug3.lean b/tests/lean/run/struct_bug3.lean new file mode 100644 index 0000000000..75bcb6f6db --- /dev/null +++ b/tests/lean/run/struct_bug3.lean @@ -0,0 +1,5 @@ +structure foo := +(f : Π {α : Type}, α) +(g : Π {α : Type}, α := @f) + +structure bar extends foo