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

fix(frontends/lean/elaborator): structure instance update with type classes

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-02 11:35:56 -07:00
parent 872360db0f
commit 838b3329ce
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1813,6 +1813,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
get_structure_instance_info(e, S_name, src, fnames, fvalues);
lean_assert(fnames.size() == fvalues.size());
name src_S_name;
unsigned src_S_nparams = 0;
if (src) {
src = visit(*src, none_expr());
synthesize_type_class_instances();
@ -1826,7 +1827,8 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
line() + format("which has type") +
pp_indent(pp_fn, type));
}
src_S_name = const_name(src_S);
src_S_name = const_name(src_S);
src_S_nparams = *inductive::get_num_params(m_env, src_S_name);
}
if (S_name.is_anonymous()) {
if (expected_type) {
@ -1879,6 +1881,9 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
if (src) {
name new_fname = src_S_name + S_fname;
expr f = copy_tag(e, mk_constant(new_fname));
f = copy_tag(e, mk_explicit(f));
for (unsigned i = 0; i < src_S_nparams; i++)
f = copy_tag(e, mk_app(f, copy_tag(e, mk_expr_placeholder())));
f = copy_tag(e, mk_app(f, *src));
try {
f = visit(f, none_expr());

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

@ -0,0 +1,10 @@
universe variables u
class foo (A : Type u) :=
(x : A)
class bla (A : Type u) extends foo A :=
(y : nat)
def ex {A : Type u} [s : foo A] : bla A :=
{ s with y := 0 }