From bf8292cb17210eafdca68554a64a62489927e310 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 24 Mar 2017 15:37:24 +0100 Subject: [PATCH] feat(frontends/lean/structure_cmd): allow local notations --- src/frontends/lean/structure_cmd.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 64a509dda4..ba73ef6bce 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -672,7 +672,8 @@ struct structure_cmd_fn { parse_field_block(binder_info()); } else { binder_info bi = m_p.parse_binder_info(); - parse_field_block(bi); + if (!m_p.parse_local_notation_decl()) + parse_field_block(bi); m_p.parse_close_binder_info(bi); } }