max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/definitional): use new type_checker

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-21 15:01:29 -07:00
parent 9cf995fae8
commit 539c31fe5a
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/definitional/brec_on.cpp
View file

@ -44,7 +44,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
if (is_inductive_predicate(env, n))
return env;
inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
old_type_checker tc(env);
type_checker tc(env);
unsigned nparams = std::get<1>(decls);
declaration ind_decl = env.get(n);
declaration rec_decl = env.get(inductive::get_elim_name(n));
@ -52,7 +52,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
unsigned nminors = *inductive::get_num_minor_premises(env, n);
unsigned ntypeformers = length(std::get<2>(decls));
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc.get_type_context(), n);
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps));
levels lvls = param_names_to_levels(tail(lps));
level_param_names blvls; // universe level parameters of ibelow/below
@ -167,7 +167,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
if (is_inductive_predicate(env, n))
return env;
inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
old_type_checker tc(env);
type_checker tc(env);
unsigned nparams = std::get<1>(decls);
declaration ind_decl = env.get(n);
declaration rec_decl = env.get(inductive::get_elim_name(n));
@ -176,7 +176,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
unsigned nminors = *inductive::get_num_minor_premises(env, n);
unsigned ntypeformers = length(std::get<2>(decls));
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc.get_type_context(), n);
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps));
levels lvls = param_names_to_levels(tail(lps));
level rlvl;

1
src/library/definitional/cases_on.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/inductive/inductive.h"
#include "kernel/type_checker.h"
#include "library/module.h"
#include "library/protected.h"
#include "library/reducible.h"