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

feat(frontends/lean/pp): pretty print neutral/unreachable terms

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-07 18:30:19 -07:00
parent e5118a3a3a
commit 93aa264060
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
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/erase_irrelevant.h"
#include "compiler/rec_fn_macro.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"
@ -551,6 +552,10 @@ optional<name> pretty_fn::is_abbreviated(expr const & e) const {
}
auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ_params) -> result {
if (is_neutral_expr(e) && m_unicode)
return format("◾");
if (is_unreachable_expr(e) && m_unicode)
return format("⊥");
if (auto it = is_abbreviated(e))
return pp_abbreviation(e, *it, false);
if (!num_ref_univ_params) {