From 9a4e04b8ca407936261ef9ab615380f17948e94e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Mar 2017 21:37:31 -0700 Subject: [PATCH] feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values --- src/frontends/lean/structure_cmd.cpp | 2 ++ tests/lean/run/unfold_default_values.lean | 10 ++++++++++ 2 files changed, 12 insertions(+) create mode 100644 tests/lean/run/unfold_default_values.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index cf7b0ad70d..92f1fb77bf 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -46,6 +46,7 @@ Author: Leonardo de Moura #include "library/constructions/projection.h" #include "library/constructions/no_confusion.h" #include "library/constructions/injective.h" +#include "library/equations_compiler/util.h" #include "library/inductive_compiler/add_decl.h" #include "library/tactic/elaborator_exception.h" #include "frontends/lean/parser.h" @@ -952,6 +953,7 @@ struct structure_cmd_fn { declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls, decl_type, decl_value, reducibility_hints::mk_abbreviation()); m_env = module::add(m_env, check(m_env, new_decl)); + m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), m_modifiers.m_is_private, decl_name, args.size()); m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true); } } diff --git a/tests/lean/run/unfold_default_values.lean b/tests/lean/run/unfold_default_values.lean new file mode 100644 index 0000000000..a615009621 --- /dev/null +++ b/tests/lean/run/unfold_default_values.lean @@ -0,0 +1,10 @@ +structure S := +(x : nat) +(y : nat := 10) + +example (a : nat) (h : 10 = a) : {S . x := 10}^.y = a := +begin + simp [S.y._default], + guard_target 10 = a, + exact h +end