From 1dc1574ad44e491726c5cab9d57fd96a91d064f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Sep 2015 20:51:06 -0700 Subject: [PATCH] fix(frontends/lean/parse_table): do not add 'no_info' annotation in tactic expressions --- src/frontends/lean/parse_table.cpp | 3 ++- tests/lean/hott/notation_with_nested_tactics.hlean | 13 +++++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 tests/lean/hott/notation_with_nested_tactics.hlean diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 11efb03da..1ba5fe954 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "library/kernel_bindings.h" #include "library/io_state_stream.h" +#include "library/tactic/expr_to_tactic.h" #include "frontends/lean/parse_table.h" #include "frontends/lean/parser.h" #include "frontends/lean/info_annotation.h" @@ -25,7 +26,7 @@ namespace notation { 3- Every other subterm is annotated with no_info. */ static expr annotate_macro_subterms(expr const & e, bool root = true) { - if (is_var(e) || is_no_info(e)) + if (is_var(e) || is_no_info(e) || is_by(e) || is_by_plus(e)) return e; if (is_binding(e)) return update_binding(e, diff --git a/tests/lean/hott/notation_with_nested_tactics.hlean b/tests/lean/hott/notation_with_nested_tactics.hlean new file mode 100644 index 000000000..97967a67b --- /dev/null +++ b/tests/lean/hott/notation_with_nested_tactics.hlean @@ -0,0 +1,13 @@ +open is_equiv +constants (A B : Type) (f : A → B) + +definition H : is_equiv f := sorry + + +definition loop [instance] [h : is_equiv f] : is_equiv f := +h + +notation `noinstances` t:max := by+ with_options [elaborator.ignore_instances true] (exact t) + +example (a : A) : let H' : is_equiv f := H in @(inv f) H' (f a) = a := +noinstances (left_inv f a)