From 5b1b11ffe0aa54ec50a2454622d322a664e241a3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Aug 2020 12:49:37 -0700
Subject: [PATCH] feat: add `isCharLit`

---
 src/Lean/Expr.lean        | 23 +++++++++++++++--------
 tests/lean/run/meta2.lean |  9 ++++++++-
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 06c9bc3889..b0c73f1181 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -427,14 +427,6 @@ def isLit : Expr → Bool
 | lit _ _ => true
 | _       => false
 
-def isNatLit : Expr → Bool
-| lit (Literal.natVal _) _ => true
-| _                        => false
-
-def isStringLit : Expr → Bool
-| lit (Literal.strVal _) _ => true
-| _                        => false
-
 def getAppFn : Expr → Expr
 | app f a _ => getAppFn f
 | e         => e
@@ -512,6 +504,21 @@ def appArg! : Expr → Expr
 | app _ a _ => a
 | _         => panic! "application expected"
 
+def isNatLit : Expr → Bool
+| lit (Literal.natVal _) _ => true
+| _                        => false
+
+def natLit? : Expr → Option Nat
+| lit (Literal.natVal v) _ => v
+| _                        => none
+
+def isStringLit : Expr → Bool
+| lit (Literal.strVal _) _ => true
+| _                        => false
+
+def isCharLit (e : Expr) : Bool :=
+e.isAppOfArity `Char.ofNat 1 && e.appArg!.isNatLit
+
 def constName! : Expr → Name
 | const n _ _ => n
 | _           => panic! "constant expected"
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index aeee391b64..1b44fdfdaa 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -734,6 +734,13 @@ check t;
 t ← mkArrayLit nat [mkNatLit 1, mkNatLit 2];
 print t;
 check t;
-pure ()
+match t.isArrayLit? with
+| some (_, xs) => do
+  check $ pure $ xs.size == 2;
+  match (xs.get! 0).isNatLit?, (xs.get! 1).isNatLit? with
+  | some 1, some 2 => pure ()
+  | _, _           => throwOther "nat lits expected"
+| none => throwOther "array lit expected"
+
 
 #eval tst42