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

fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account

Browse source 
fixes #466
This commit is contained in:
Leonardo de Moura 2015-03-11 08:29:54 -07:00
parent 1244f01518
commit 4c6b0dc0e5
2 changed files with 25 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/tactic/expr_to_tactic.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "library/annotation.h"
#include "library/string.h"
#include "library/explicit.h"
#include "library/num.h"
#include "library/constants.h"
#include "library/kernel_serializer.h"
@ -113,12 +114,19 @@ void check_tactic_expr(expr const & e, char const * error_msg) {
name const & tactic_expr_to_id(expr e, char const * error_msg) {
if (is_tactic_expr(e))
e = get_tactic_expr_expr(e);
if (is_constant(e))
if (is_constant(e)) {
return const_name(e);
else if (is_local(e))
} else if (is_local(e)) {
return local_pp_name(e);
else
} else if (is_as_atomic(e)) {
e = get_app_fn(get_as_atomic_arg(e));
if (is_explicit(e))
e = get_explicit_arg(e);
return tactic_expr_to_id(e, error_msg);
} else {
throw expr_to_tactic_exception(e, error_msg);
}
}
static expr * g_expr_list_cons = nullptr;

14
tests/lean/run/466.lean Normal file
View file

@ -0,0 +1,14 @@
open eq
context
parameter (A : Type)
definition foo (a : A) : a = a := refl a
definition bar (a : A) : foo a = refl a :=
begin
unfold foo,
apply rfl
end
end