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

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

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-22 17:03:14 -08:00
parent 96f391dda2
commit 2a294bcc17
2 changed files with 13 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

@ -1537,7 +1537,7 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
expr const & from_type = mlocal_type(from);
// fix user visible name
expr d0 = binding_domain(goal);
expr goal_domain = visit(d0, cs);
expr goal_domain = ensure_type(visit(d0, cs), cs);
if (is_placeholder(d0) && !is_explicit_placeholder(d0))
save_binder_type(d0, goal_domain);
expr new_from = ::lean::mk_local(mlocal_name(from), binding_name(goal), goal_domain, binder_info());

12
tests/lean/hott/996.hlean Normal file
View file

@ -0,0 +1,12 @@
import types.pointed
open pointed
variable A : Type*
variable a : A
-- Type* is notation for the type of pointed types (types with a specified point in them)
definition ex (A : Type*) (v : Σ(x : A), x = x) : v = v :=
obtain (x : A) (p : _), from v,
rfl
print ex