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

feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-07 19:58:53 -07:00
parent 2631979f5c
commit cbdfb0dcdc
2 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -462,8 +462,19 @@ class elaborator {
try { try {
bool no_info = true; bool no_info = true;
new_scope s(m_elab, m_state, no_info); new_scope s(m_elab, m_state, no_info);
expr type = m_meta_type;
buffer<expr> locals;
while (is_pi(type)) {
expr local = ::lean::mk_local(m_elab.m_ngen.next(), binding_name(type), binding_domain(type),
binding_info(type));
if (binding_info(type).is_contextual())
m_elab.m_context.add_local(local);
m_elab.m_full_context.add_local(local);
locals.push_back(local);
type = instantiate(binding_body(type), local);
}
pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc. pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
expr r = rcs.first; expr r = Fun(locals, rcs.first);
buffer<constraint> cs; buffer<constraint> cs;
to_buffer(rcs.second, m_jst, cs); to_buffer(rcs.second, m_jst, cs);
return optional<constraints>(cons(mk_eq_cnstr(m_meta, r, m_jst, m_relax_main_opaque), return optional<constraints>(cons(mk_eq_cnstr(m_meta, r, m_jst, m_relax_main_opaque),

10
tests/lean/run/dfun_tst.lean Normal file
View file

@ -0,0 +1,10 @@
import logic data.prod data.vector
open prod nat inhabited vec
theorem tst1 : inhabited (vec nat 2)
theorem tst2 : inhabited (Prop × (Π n : nat, vec nat n))
(*
print(get_env():find("tst2"):value())
*)