From 0137500c832e01147d5e327f743abb1aba6ef71c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2020 08:28:22 -0800
Subject: [PATCH] fix: missing `decodeStrLit` and `decodeCharLit`

They are just placeholders.
---
 src/Init/Lean/Syntax.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 36cb3a89fa..8e81a87af0 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -385,21 +385,29 @@ mkStxNumLit (toString val)
 
 namespace Syntax
 
+def decodeStrLit (s : String) : String :=
+ -- TODO handle escape seqs
+s.extract 1 (s.bsize - 1)
+
 def isStrLit? : Syntax → Option String
 | Syntax.node k args   =>
   if k == strLitKind && args.size == 1 then
     match args.get! 0 with
-    | (Syntax.atom _ val) => some val
+    | (Syntax.atom _ val) => some (decodeStrLit val)
     | _ => none
   else
     none
 | _ => none
 
+def decodeCharLit (s : String) : Char :=
+-- TODO handle escape seqs
+s.get 1
+
 def isCharLit? : Syntax → Option Char
 | Syntax.node k args   =>
   if k == charLitKind && args.size == 1 then
     match args.get! 0 with
-    | (Syntax.atom _ val) => some (val.get 1)
+    | (Syntax.atom _ val) => some (decodeCharLit val)
     | _ => none
   else
     none