diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 8d682fb8c..5b37b9f84 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -66,6 +66,9 @@ public:
};
expr const Bool = mk_value(*(new bool_type_value()));
expr mk_bool_type() { return Bool; }
+bool is_bool(expr const & e) {
+ return e == Bool || (is_constant(e) && const_name(e) == to_value(Bool).get_name());
+}
// =======================================
// =======================================
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 7d2ed1e4d..6d194d275 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -31,6 +31,7 @@ extern expr const TypeU;
/** \brief Return the Lean Boolean type. */
expr mk_bool_type();
extern expr const Bool;
+bool is_bool(expr const & e);
/** \brief Create a Lean Boolean value (true/false) */
expr mk_bool_value(bool v);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index d42387dc5..b25eb2b1e 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -69,12 +69,12 @@ class type_checker::imp {
expr check_type(expr const & e, expr const & s, context const & ctx) {
if (is_type(e))
return e;
- if (e == Bool)
+ if (is_bool(e))
return Type();
expr u = normalize(e, ctx);
if (is_type(u))
return u;
- if (u == Bool)
+ if (is_bool(u))
return Type();
if (has_metavar(u) && m_menv) {
justification jst = mk_type_expected_justification(ctx, s);
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index f6e2afa95..036abbb3e 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -659,7 +659,7 @@ class elaborator::imp {
an equality constraint.
*/
bool is_actual_lower(expr const & a) {
- return is_type(a) || is_metavar(a) || a == Bool || (is_pi(a) && is_actual_lower(abst_body(a)));
+ return is_type(a) || is_metavar(a) || is_bool(a) || (is_pi(a) && is_actual_lower(abst_body(a)));
}
/**
@@ -942,7 +942,7 @@ class elaborator::imp {
return
is_convertible(c) &&
is_metavar(convertible_to(c)) &&
- (convertible_from(c) == Bool || is_type(convertible_from(c)));
+ (is_bool(convertible_from(c)) || is_type(convertible_from(c)));
}
/** \brief Process constraint of the form ctx |- a << ?m, where \c a is Type or Bool */
@@ -952,7 +952,7 @@ class elaborator::imp {
// We approximate and only consider the most useful ones.
justification new_jst(new destruct_justification(c));
unification_constraint new_c;
- if (a == Bool) {
+ if (is_bool(a)) {
expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
} else {
@@ -1111,7 +1111,7 @@ class elaborator::imp {
process_simple_ho_match(ctx, b, a, false, c))
return true;
- if (!eq && a == Bool && is_type(b))
+ if (!eq && is_bool(a) && is_type(b))
return true;
if (a.kind() == b.kind()) {
@@ -1254,9 +1254,9 @@ class elaborator::imp {
push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
return true;
}
- if (lhs1 == Bool)
+ if (is_bool(lhs1))
lhs1 = Type();
- if (lhs2 == Bool)
+ if (is_bool(lhs2))
lhs2 = Type();
if (is_type(lhs1) && is_type(lhs2)) {
justification new_jst(new normalize_justification(c));
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index e567775db..719b31403 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -38,12 +38,12 @@ class type_inferer::imp {
expr check_type(expr const & e, expr const & s, context const & ctx) {
if (is_type(e))
return e;
- if (e == Bool)
+ if (is_bool(e))
return Type();
expr u = normalize(e, ctx);
if (is_type(u))
return u;
- if (u == Bool)
+ if (is_bool(u))
return Type();
if (has_metavar(u) && m_menv) {
justification jst = mk_type_expected_justification(ctx, s);
@@ -237,6 +237,15 @@ public:
m_menv = nullptr;
m_menv_timestamp = 0;
}
+
+ bool is_proposition(expr const & e, context const & ctx) {
+ buffer uc;
+ expr t = operator()(e, ctx, nullptr, uc);
+ if (is_bool(t))
+ return true;
+ else
+ return is_bool(normalize(e, ctx));
+ }
};
type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {}
type_inferer::~type_inferer() {}
@@ -248,9 +257,7 @@ expr type_inferer::operator()(expr const & e, context const & ctx) {
return operator()(e, ctx, nullptr, uc);
}
bool type_inferer::is_proposition(expr const & e, context const & ctx) {
- expr t = operator()(e, ctx);
- // TODO(Leo): consider replacing the following test with is_convertible(t, Bool);
- return t == Bool;
+ return m_ptr->is_proposition(e, ctx);
}
void type_inferer::clear() { m_ptr->clear(); }
}
diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp
index f8cd0562b..bcb8bd616 100644
--- a/src/tests/frontends/lean/frontend.cpp
+++ b/src/tests/frontends/lean/frontend.cpp
@@ -136,13 +136,13 @@ static void tst9() {
f.add_definition("x", Bool, True);
object const & obj = f.get_object("x");
lean_assert(obj.get_name() == "x");
- lean_assert(obj.get_type() == Bool);
+ lean_assert(is_bool(obj.get_type()));
lean_assert(obj.get_value() == True);
try { f.get_object("y"); lean_unreachable(); }
catch (exception &) {}
lean_assert(!f.find_object("y"));
f.add_definition("y", False);
- lean_assert(f.find_object("y").get_type() == Bool);
+ lean_assert(is_bool(f.find_object("y").get_type()));
lean_assert(f.has_object("y"));
lean_assert(!f.has_object("z"));
bool found = false;
diff --git a/src/tests/library/type_inferer.cpp b/src/tests/library/type_inferer.cpp
index 307dcee86..2a26acc1e 100644
--- a/src/tests/library/type_inferer.cpp
+++ b/src/tests/library/type_inferer.cpp
@@ -34,7 +34,7 @@ static void tst1() {
env.add_var("f", Int >> (Int >> Int));
lean_assert(type_of(f(a, a)) == Int);
lean_assert(type_of(f(a)) == Int >> Int);
- lean_assert(type_of(And(a, f(a))) == Bool);
+ lean_assert(is_bool(type_of(And(a, f(a)))));
lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int);
lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int);
lean_assert(type_of(Type()) == Type(level() + 1));