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

fix(checker/text_import): commit 3c1ccc9 broke it

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-31 14:59:36 -07:00
parent 112d1da8d0
commit 8a918a2a14
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/checker/text_import.cpp
View file

@ -61,7 +61,7 @@ struct text_importer {
auto ls = read_level_params(in);
inductive::inductive_decl decl(m_name.at(name_idx), ls, num_params, m_expr.at(type_idx), to_list(intros));
m_env = inductive::add_inductive(m_env, decl, true).first;
m_env = inductive::add_inductive(m_env, decl, false).first;
}
void handle_def(std::istream & in) {
@ -72,7 +72,7 @@ struct text_importer {
auto decl =
type_checker(m_env).is_prop(m_expr.at(type_idx)) ?
mk_theorem(m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx)) :
mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, true);
mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, false);
m_env = m_env.add(check(m_env, decl));
}