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

feat(frontends/lean/elaborator): add hard coded coercion from bool to Prop

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-28 15:38:22 -07:00
parent b5f006d229
commit a7c8cbc548
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/elaborator.cpp
View file

@ -298,6 +298,11 @@ optional<expr> 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();
}

7
tests/lean/run/elab_bool.lean Normal file
View file

@ -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