From 299fd5c9197c80b74c6a46bc9cdf8c7a6ea5b2bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 May 2015 10:38:42 -0700 Subject: [PATCH] feat(frontends/lean/pp): pp inaccessible patterns --- src/frontends/lean/pp.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index c699c873c..8fdff1ea0 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/constants.h" #include "library/replace_visitor.h" +#include "library/definitional/equations.h" #include "frontends/lean/pp.h" #include "frontends/lean/util.h" #include "frontends/lean/token_table.h" @@ -672,6 +673,10 @@ auto pretty_fn::pp_explicit(expr const & e) -> result { auto pretty_fn::pp_macro(expr const & e) -> result { if (is_explicit(e)) { return pp_explicit(e); + } else if (is_inaccessible(e)) { + format li = m_unicode ? format("⌞") : format("?("); + format ri = m_unicode ? format("⌟") : format(")"); + return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri))); } else if (is_annotation(e)) { return pp(get_annotation_arg(e)); } else {