michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parse_table): do not add 'no_info' annotation in tactic expressions

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-02 20:51:06 -07:00
parent 634c0b5e9d
commit 1dc1574ad4
2 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parse_table.cpp
View file

@ -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,

13
tests/lean/hott/notation_with_nested_tactics.hlean Normal file
View file

@ -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)