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

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

Return .done for Char values. We don't want to unfold in the symbolic evaluator. In regular simp, we want to prevent the nested raw literal from being converted into a OfNat.ofNat application. TODO: cleanup

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.