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

feat(library/definitional/no_confusion): add [unfold] hint to no_confusion

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-07 20:07:13 -07:00
parent 26574e29a9
commit 6ffbb05118
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/definitional/no_confusion.cpp
View file

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/reducible.h"
#include "library/constants.h"
#include "library/normalize.h"
namespace lean {
static void throw_corrupted(name const & n) {
@ -201,6 +202,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
no_confusion_type_args.push_back(P);
no_confusion_type_args.push_back(v1);
no_confusion_type_args.push_back(v1);
unsigned unfold_hint_idx = no_confusion_type_args.size();
expr no_confusion_type_app = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), no_confusion_type_args);
expr type_former = Fun(type_former_args, no_confusion_type_app);
// create cases_on
@ -273,6 +275,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
new_env = add_unfold_hint(new_env, no_confusion_name, unfold_hint_idx);
return add_protected(new_env, no_confusion_name);
}
}

3
src/library/normalize.h
View file

@ -41,6 +41,9 @@ expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&
Of course, kernel opaque constants are not unfolded.
*/
environment add_unfold_hint(environment const & env, name const & n, list<unsigned> const & idxs, bool persistent = true);
inline environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent = true) {
return add_unfold_hint(env, n, to_list(idx), persistent);
}
environment erase_unfold_hint(environment const & env, name const & n, bool persistent = true);
/** \brief Retrieve the hint added with the procedure add_unfold_hint. */
list<unsigned> has_unfold_hint(environment const & env, name const & d);