From a7c8cbc548a5cd0debb26472e2511139db1dcc12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Jul 2016 15:38:22 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): add hard coded coercion from bool to Prop --- src/frontends/lean/elaborator.cpp | 5 +++++ tests/lean/run/elab_bool.lean | 7 +++++++ 2 files changed, 12 insertions(+) create mode 100644 tests/lean/run/elab_bool.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index db47c96c25..c5d9751b95 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -298,6 +298,11 @@ optional elaborator::ensure_has_type(expr const & e, expr const & e_type, type_context::approximate_scope scope(m_ctx); if (is_def_eq(e_type, type)) return some_expr(e); + + // Coercion from bool => Prop + if (is_constant(e_type, get_bool_name()) && type == mk_Prop()) + return some_expr(mk_eq(m_ctx, e, mk_constant(get_bool_tt_name()))); + return none_expr(); } diff --git a/tests/lean/run/elab_bool.lean b/tests/lean/run/elab_bool.lean new file mode 100644 index 0000000000..3baf799c6d --- /dev/null +++ b/tests/lean/run/elab_bool.lean @@ -0,0 +1,7 @@ +variable b : bool + +#elab if b then tt else ff + +#elab if b && b then tt else ff + +#elab if b ∧ b then tt else ff