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.

Equations

• Char.fromExpr? e = liftM (Lean.Meta.getCharValue? e)

@[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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Char.reduceToLower = Char.reduceUnary `Char.toLower Char.toLower

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

Equations

• Char.reduceToUpper = Char.reduceUnary `Char.toUpper Char.toUpper

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

Equations

• Char.reduceToNat = Char.reduceUnary `Char.toNat Char.toNat

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

Equations

• Char.reduceIsWhitespace = Char.reduceUnary `Char.isWhitespace Char.isWhitespace

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

Equations

• Char.reduceIsUpper = Char.reduceUnary `Char.isUpper Char.isUpper

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

Equations

• Char.reduceIsLower = Char.reduceUnary `Char.isLower Char.isLower

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

Equations

• Char.reduceIsAlpha = Char.reduceUnary `Char.isAlpha Char.isAlpha

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

Equations

• Char.reduceIsDigit = Char.reduceUnary `Char.isDigit Char.isDigit

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

Equations

• Char.reduceIsAlphaNum = Char.reduceUnary `Char.isAlphanum Char.isAlphanum

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

Equations

• Char.reduceToString = Char.reduceUnary `ToString.toString toString 3

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Char.reduceLT = Char.reduceBinPred `LT.lt 4 fun (x1 x2 : Char) => decide (x1 < x2)

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

Equations

• Char.reduceLE = Char.reduceBinPred `LE.le 4 fun (x1 x2 : Char) => decide (x1 ≤ x2)

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

Equations

• Char.reduceGT = Char.reduceBinPred `GT.gt 4 fun (x1 x2 : Char) => decide (x1 > x2)

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

Equations

• Char.reduceGE = Char.reduceBinPred `GE.ge 4 fun (x1 x2 : Char) => decide (x1 ≥ x2)

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

Equations

• Char.reduceEq = Char.reduceBinPred `Eq 3 fun (x1 x2 : Char) => decide (x1 = x2)

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

Equations

• Char.reduceNe = Char.reduceBinPred `Ne 3 fun (x1 x2 : Char) => decide (x1 ≠ x2)

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

Equations

• Char.reduceBEq = Char.reduceBoolPred `BEq.beq 4 fun (x1 x2 : Char) => x1 == x2

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

Equations

• Char.reduceBNe = Char.reduceBoolPred `bne 4 fun (x1 x2 : Char) => x1 != x2

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.