def String.reduceAppend : Lean.Meta.Simp.DSimproc

Equations

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

def String.reduceOfList : Lean.Meta.Simp.DSimproc

Equations

• String.reduceOfList e = if e.isAppOfArity `String.ofList 1 = true then String.reduceListChar✝ e.appArg! "" else pure Lean.TransformStep.continue

def String.reduceToList : Lean.Meta.Simp.DSimproc

Equations

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

def String.reducePush : Lean.Meta.Simp.DSimproc

Equations

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

def String.reduceSingleton : Lean.Meta.Simp.DSimproc

Equations

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

def String.reduceToSingleton : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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