michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/definitional/projection): add "unfold-c" hint to projections

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-06 12:39:57 -08:00
parent 1bd1f94542
commit 7205382f8c
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/definitional/projection.cpp
View file

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "library/projection.h"
#include "library/module.h"
#include "library/util.h"
#include "library/normalize.h"
#include "library/definitional/projection.h"
namespace lean {
@ -134,6 +135,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
opaque, rec_decl.get_module_idx(), use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, proj_name, reducible_status::On);
new_env = add_unfold_c_hint(new_env, proj_name, nparams);
new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);
expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
intro_type = instantiate(binding_body(intro_type), proj);