From fa1bf40d0fff06e655cd500998b74f1a6cf32079 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Oct 2014 15:09:24 -0700 Subject: [PATCH] fix(library/definitional): make sure argument is an inductive datatype --- src/library/definitional/induction_on.cpp | 3 +++ src/library/definitional/rec_on.cpp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp index 971bff19e4..56a078e211 100644 --- a/src/library/definitional/induction_on.cpp +++ b/src/library/definitional/induction_on.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sstream.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" @@ -14,6 +15,8 @@ namespace lean { environment mk_induction_on(environment const & env, name const & n) { if (!env.impredicative()) throw exception("induction_on generation failed, Prop/Type.{0} is not impredicative in the given environment"); + if (!inductive::is_inductive_decl(env, n)) + throw exception(sstream() << "error in 'induction_on' generation, '" << n << "' is not an inductive datatype"); name rec_on_name(n, "rec_on"); name induction_on_name(n, "induction_on"); name_generator ngen; diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index 4291a7ba59..98d423dd98 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sstream.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -14,6 +15,8 @@ Author: Leonardo de Moura namespace lean { environment mk_rec_on(environment const & env, name const & n) { + if (!inductive::is_inductive_decl(env, n)) + throw exception(sstream() << "error in 'rec_on' generation, '" << n << "' is not an inductive datatype"); name rec_on_name(n, "rec_on"); name_generator ngen; declaration rec_decl = env.get(inductive::get_elim_name(n));