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

fix(library/definitional): make sure argument is an inductive datatype

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-25 15:09:24 -07:00
parent 758a17ab23
commit fa1bf40d0f
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/induction_on.cpp
View file

@ -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;

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

@ -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));