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

feat(checker/text_import): import definitions whose type is in Prop as theorems

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-31 10:19:08 +01:00
parent f404e8a2be
commit 7d14cb640c
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/checker/text_import.cpp
View file

@ -68,9 +68,13 @@ struct text_importer {
unsigned name_idx, type_idx, val_idx;
in >> name_idx >> type_idx >> val_idx;
auto ls = read_level_params(in);
m_env = m_env.add(check(m_env, mk_definition(m_env,
m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx),
true, true), true));
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);
m_env = m_env.add(check(m_env, decl, true));
}
void handle_ax(std::istream & in) {