def Char.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option Char)

Return some c if e is a Char.ofNat-application that encodes the character c.

@[inline]

def Char.reduceUnary {α : Type u_1} [Lean.ToExpr α] (declName : Lean.Name) (op : Char → α) (arity : Nat := 1) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[inline]

def Char.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : Char → Char → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

@[inline]

def Char.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : Char → Char → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def Char.reduceToLower : Lean.Meta.Simp.DSimproc

def Char.reduceToUpper : Lean.Meta.Simp.DSimproc

def Char.reduceToNat : Lean.Meta.Simp.DSimproc

def Char.reduceIsWhitespace : Lean.Meta.Simp.DSimproc

def Char.reduceIsUpper : Lean.Meta.Simp.DSimproc

def Char.reduceIsLower : Lean.Meta.Simp.DSimproc

def Char.reduceIsAlpha : Lean.Meta.Simp.DSimproc

def Char.reduceIsDigit : Lean.Meta.Simp.DSimproc

def Char.reduceIsAlphaNum : Lean.Meta.Simp.DSimproc

def Char.reduceToString : Lean.Meta.Simp.DSimproc

def Char.reduceVal : Lean.Meta.Simp.DSimproc

def Char.reduceLT : Lean.Meta.Simp.Simproc

def Char.reduceLE : Lean.Meta.Simp.Simproc

def Char.reduceGT : Lean.Meta.Simp.Simproc

def Char.reduceGE : Lean.Meta.Simp.Simproc

def Char.reduceEq : Lean.Meta.Simp.Simproc

def Char.reduceNe : Lean.Meta.Simp.Simproc

def Char.reduceBEq : Lean.Meta.Simp.DSimproc

def Char.reduceBNe : Lean.Meta.Simp.DSimproc

def Char.isValue : Lean.Meta.Simp.DSimproc

Returns .done for Char values.

These values should not be unfolded in the symbolic evaluator.

In regular simp, the nested raw literal should be prevented from being converted into an OfNat.ofNat application.

def Char.reduceOfNatAux : Lean.Meta.Simp.DSimproc

def Char.reduceDefault : Lean.Meta.Simp.DSimproc