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

fix(frontends/lean/structure_cmd): disable def-eq check of pre-expressions

Browse source
This commit is contained in:
Gabriel Ebner 2017-08-02 10:26:25 +01:00 • committed by Leonardo de Moura
parent c500f9497d
commit fe5cb0106c
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/structure_cmd.cpp
View file

@ -688,6 +688,9 @@ struct structure_cmd_fn {
expr fdefault = mk_field_default_value(full_fname);
if (!field.m_default_val) {
field.m_default_val = fdefault;
}
// TODO(gabriel): the defeq check below is completely broken because it compares pre-expressions
/*
} else if (field.m_default_val && !m_ctx.is_def_eq(*field.m_default_val, fdefault)) {
expr prev_default = *field.m_default_val;
throw generic_exception(parent, [=](formatter const &fmt) {
@ -702,6 +705,7 @@ struct structure_cmd_fn {
return r;
});
}
*/
}
fmap_start++;
}