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

feat(frontends/lean/builtin_cmds): display '[forward]' annotation for heuristic instantiation lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-25 17:53:13 -08:00
parent 996a660de8
commit 0ceaf0b4fe
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_cmds.cpp
View file

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