michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/elaborator): fixes #965

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-04 13:41:21 -08:00
parent 42fbc63bb6
commit 0268f92eb4
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -969,7 +969,7 @@ expr elaborator::visit_lambda(expr const & e, constraint_seq & cs) {
expr elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) {
constraint_seq t_cs;
expr t = visit(get_typed_expr_type(e), t_cs);
expr t = ensure_type(visit_expecting_type(get_typed_expr_type(e), t_cs), t_cs);
constraint_seq v_cs;
expr v = visit_expecting_type_of(get_typed_expr_expr(e), t, v_cs);
expr v_type = infer_type(v, v_cs);

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

@ -0,0 +1,7 @@
import algebra.bundled
variable G : Group
check (1 : G)
check (1 : Group.carrier G)
set_option pp.coercions true
check (1 : G)
check (1 : Group.carrier G)