max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/pp): pretty print recursive calls

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-05 18:10:55 -07:00
parent 9a247d6ac4
commit 454ec00f17
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -35,6 +35,7 @@ Author: Leonardo de Moura
#include "library/replace_visitor.h"
#include "library/definitional/equations.h"
#include "compiler/comp_irrelevant.h"
#include "compiler/rec_fn_macro.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"
#include "frontends/lean/token_table.h"
@ -832,6 +833,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
return m_unicode ? format("◾") : format("irrel");
} else if (is_annotation(e)) {
return pp(get_annotation_arg(e));
} else if (is_rec_fn_macro(e)) {
return format("[") + format(get_rec_fn_name(e)) + format("]");
} else {
// TODO(Leo): have macro annotations
// fix macro<->pp interface