feat: add isCharLit

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"

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