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

feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-27 21:37:31 -07:00
parent 36c7d46c34
commit 9a4e04b8ca
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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);
}
}

10
tests/lean/run/unfold_default_values.lean Normal file
View file

@ -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