From b07b82cf43a565ecfdfaba9d352b02d8ceffa2ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Nov 2014 15:03:30 -0800 Subject: [PATCH] fix(library/definitional): marking cases_on and rec_on as reducible The idea is to avoid counter-intuitive behavior --- src/library/definitional/cases_on.cpp | 2 ++ src/library/definitional/rec_on.cpp | 5 ++++- tests/lean/run/elab_failure.lean | 15 +++++++++++++++ 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/elab_failure.lean diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 57bef3eeeb..a80400f6be 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/module.h" #include "library/protected.h" +#include "library/reducible.h" namespace lean { static void throw_corrupted(name const & n) { @@ -178,6 +179,7 @@ environment mk_cases_on(environment const & env, name const & n) { declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, opaque, rec_decl.get_module_idx(), use_conv_opt); environment new_env = module::add(env, check(env, new_d)); + new_env = set_reducible(new_env, cases_on_name, reducible_status::On); return add_protected(new_env, cases_on_name); } } diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index 98d423dd98..c2cd749763 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" #include "library/module.h" +#include "library/reducible.h" #include "library/protected.h" namespace lean { @@ -53,8 +54,10 @@ environment mk_rec_on(environment const & env, name const & n) { bool opaque = false; bool use_conv_opt = true; environment new_env = module::add(env, - check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val, + check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), + rec_on_type, rec_on_val, opaque, rec_decl.get_module_idx(), use_conv_opt))); + new_env = set_reducible(new_env, rec_on_name, reducible_status::On); return add_protected(new_env, rec_on_name); } } diff --git a/tests/lean/run/elab_failure.lean b/tests/lean/run/elab_failure.lean new file mode 100644 index 0000000000..957dc8fcfd --- /dev/null +++ b/tests/lean/run/elab_failure.lean @@ -0,0 +1,15 @@ +import data.nat.basic data.bool +open bool nat +reducible nat.rec_on +definition is_eq (a b : nat) : bool := +nat.rec_on a + (λ b, nat.cases_on b tt (λb₁, ff)) + (λ a₁ r₁ b, nat.cases_on b ff (λb₁, r₁ b₁)) + b + +example (a₁ : nat) (b : nat) : true := +@nat.cases_on (λ (n : nat), true) b + true.intro + (λ (b₁ : _), + have aux : is_eq a₁ b₁ = is_eq (succ a₁) (succ b₁), from rfl, + true.intro)