From 8fd8ff27736262fbc91dc92ae3503f8b34acdda0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 27 Sep 2015 23:43:59 +0200 Subject: [PATCH] fix(frontends/lean): ignore reserved notation for pretty printing Because reserved notation uses `Prop` as a dummy expression, pretty printing `Prop` unnecessarily invokes pp_notation on every reserved notation entry. --- src/frontends/lean/pp.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 5acbd666e4..77aaf28695 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1221,6 +1221,8 @@ auto pretty_fn::pp_notation(expr const & e) -> optional { if (!m_notation || is_var(e)) return optional(); for (notation_entry const & entry : get_notation_entries(m_env, head_index(e))) { + if (entry.group() != notation_entry_group::Main) + continue; if (!m_unicode && !entry.is_safe_ascii()) continue; // ignore this notation declaration since unicode support is not enabled unsigned num_params = get_num_parameters(entry);