From 01acecf9beb5ee92808816214957eeaa236f6b21 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Mar 2020 11:04:43 -0700
Subject: [PATCH] chore: helper predicates

---
 src/Init/Lean/Expr.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index fe3309c6aa..324f4c92ae 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -428,6 +428,18 @@ def isMData : Expr → Bool
 | mdata _ _ _ => true
 | _           => false
 
+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