From ef529c660f6f1d54663168883dbbb40baa459e23 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jan 2015 18:44:47 -0800 Subject: [PATCH] fix(library/definitional/no_confusion): mark no_confusion as reducible Auxiliary definitions should be marked as reducible --- src/library/definitional/no_confusion.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index c01c487748..72c7bc51f3 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/module.h" #include "library/util.h" +#include "library/reducible.h" namespace lean { static void throw_corrupted(name const & n) { @@ -139,6 +140,7 @@ optional mk_no_confusion_type(environment const & env, name const & declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, opaque, ind_decl.get_module_idx(), use_conv_opt); environment new_env = module::add(env, check(env, new_d)); + new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::On); return some(add_protected(new_env, no_confusion_type_name)); } @@ -278,6 +280,7 @@ environment mk_no_confusion(environment const & env, name const & n) { declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, opaque, no_confusion_type_decl.get_module_idx(), 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::On); return add_protected(new_env, no_confusion_name); } }