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

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

Equations

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

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

• Char.isValue e = do let __do_lift ← Lean.Char.fromExpr? e if __do_lift.isSome = true then pure (Lean.TransformStep.done e) else pure Lean.TransformStep.continue

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.

def Char.Nat.reduceDigitCharEq : Lean.Meta.Simp.Simproc

Simplifies Nat.digitChar n = c to False when c is a concrete character not in the range of digitChar (i.e., not one of '0'-'9', 'a'-'f', '*').

Equations

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

def Char.Nat.reduceEqDigitChar : Lean.Meta.Simp.Simproc

Simplifies c = Nat.digitChar n to False when c is a concrete character not in the range of digitChar (i.e., not one of '0'-'9', 'a'-'f', '*').

Equations

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