From ffe9b3c5d6a678e73ae32865a66cf189ba0bafb3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Nov 2016 11:58:11 -0800
Subject: [PATCH] fix(frontends/lean/pp): char literals

---
 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 d649564a18..cc66c92099 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1202,6 +1202,7 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) ->
         }
         if (m_strings) {
             if (auto r = to_string(e)) return pp_string_literal(*r);
+            if (auto r = to_char(e))   return pp_char_literal(*r);
         }
         expr const & f = app_fn(e);
         if (is_implicit(f)) {
@@ -1579,6 +1580,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     }
     if (m_strings) {
         if (auto r = to_string(e)) return pp_string_literal(*r);
+        if (auto r = to_char(e))   return pp_char_literal(*r);
     }
     if (auto t = is_proof(e)) {
         return pp_proof_type(*t);