From fe5cb0106c79a716c841a8a09a5fa8df0d17ecc5 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 2 Aug 2017 10:26:25 +0100 Subject: [PATCH] fix(frontends/lean/structure_cmd): disable def-eq check of pre-expressions --- src/frontends/lean/structure_cmd.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 26c3858a93..02309a0ea2 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -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++; }