From e2fa981e89594a46ae6d67cf811ade27768051c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Oct 2014 18:08:13 -0700
Subject: [PATCH] fix(frontends/lean/pp): avoid parentheses around atomic
 notation

---
 src/frontends/lean/pp.cpp           | 12 ++++++++++++
 tests/lean/run/atomic_notation.lean |  6 ++++++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/lean/run/atomic_notation.lean

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index add6e71fd..1afa640b4 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -700,9 +700,21 @@ static bool add_extra_space(name const & tk) {
     return tk != "," && tk != "(" && tk != ")";
 }
 
+static bool is_atomic_notation(notation_entry const & entry) {
+    if (!entry.is_nud())
+        return false;
+    list<notation::transition> const & ts = entry.get_transitions();
+    if (!is_nil(tail(ts)))
+        return false;
+    return head(ts).get_action().kind() == notation::action_kind::Skip;
+}
+
 auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>> & args) -> optional<result> {
     if (entry.is_numeral()) {
         return some(result(format(entry.get_num())));
+    } else if (is_atomic_notation(entry)) {
+        format fmt   = format(head(entry.get_transitions()).get_token());
+        return some(result(fmt));
     } else {
         using notation::transition;
         buffer<transition> ts;
diff --git a/tests/lean/run/atomic_notation.lean b/tests/lean/run/atomic_notation.lean
new file mode 100644
index 000000000..a75c96abb
--- /dev/null
+++ b/tests/lean/run/atomic_notation.lean
@@ -0,0 +1,6 @@
+import logic data.num
+open num
+constant f : num → num
+notation `o`:1 := 10
+check o + 1
+check f o + o + o