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

Equations

• String.fromExpr? e = pure (Lean.Meta.getStringValue? e)

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

Equations

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

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

Equations

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

@[inline]

def String.reduceBinPred (declName : Lake.Name) (arity : Nat) (op : String → String → 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 String.reduceBoolPred (declName : Lake.Name) (arity : Nat) (op : String → String → 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 String.reduceLT : Lean.Meta.Simp.Simproc

Equations

• String.reduceLT = String.reduceBinPred `LT.lt 4 fun (x x_1 : String) => decide (x < x_1)

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

Equations

• String.reduceLE = String.reduceBinPred `LE.le 4 fun (x x_1 : String) => decide (x ≤ x_1)

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

Equations

• String.reduceGT = String.reduceBinPred `GT.gt 4 fun (x x_1 : String) => decide (x > x_1)

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

Equations

• String.reduceGE = String.reduceBinPred `GE.ge 4 fun (x x_1 : String) => decide (x ≥ x_1)

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

Equations

• String.reduceEq = String.reduceBinPred `Eq 3 fun (x x_1 : String) => decide (x = x_1)

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

Equations

• String.reduceNe = String.reduceBinPred `Ne 3 fun (x x_1 : String) => decide (x ≠ x_1)

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

Equations

• String.reduceBEq = String.reduceBoolPred `BEq.beq 4 fun (x x_1 : String) => x == x_1

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

Equations

• String.reduceBNe = String.reduceBoolPred `bne 4 fun (x x_1 : String) => x != x_1