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

• String.reduceMk e = if e.isAppOfArity `String.mk 1 = true then do let y ← pure PUnit.unit (fun (y : PUnit) => String.reduceListChar✝ e.appArg! "") y else pure Lean.TransformStep.continue

@[inline]

def String.reduceBinPred (declName : Lean.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 : Lean.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

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

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

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