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