From 7d14cb640c3971094e64ca61db73b185a2c667e5 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 31 Jan 2017 10:19:08 +0100 Subject: [PATCH] feat(checker/text_import): import definitions whose type is in Prop as theorems --- src/checker/text_import.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp index e606dc265f..d3f2e5c117 100644 --- a/src/checker/text_import.cpp +++ b/src/checker/text_import.cpp @@ -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) {