From 4c6b0dc0e514447c5ea2b8566fdc70342aaf238e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Mar 2015 08:29:54 -0700 Subject: [PATCH] fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account fixes #466 --- src/library/tactic/expr_to_tactic.cpp | 14 +++++++++++--- tests/lean/run/466.lean | 14 ++++++++++++++ 2 files changed, 25 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/466.lean diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 5715f18f8c..8df152ddc2 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -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; diff --git a/tests/lean/run/466.lean b/tests/lean/run/466.lean new file mode 100644 index 0000000000..4f8f754637 --- /dev/null +++ b/tests/lean/run/466.lean @@ -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