From 0ceaf0b4fe9ad10002bd4c4a503e775270a5c890 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Nov 2015 17:53:13 -0800 Subject: [PATCH] feat(frontends/lean/builtin_cmds): display '[forward]' annotation for heuristic instantiation lemmas --- src/frontends/lean/builtin_cmds.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c36422372..e575c753a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -263,6 +263,8 @@ static void print_attributes(parser const & p, name const & n) { out << " [backward]"; if (is_no_pattern(env, n)) out << " [no_pattern]"; + if (is_hi_lemma(env, n)) + out << " [forward]"; switch (get_reducible_status(env, n)) { case reducible_status::Reducible: out << " [reducible]"; break; case reducible_status::Irreducible: out << " [irreducible]"; break;