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

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

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

@[inline]

def String.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : String → String → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

@[inline]

def String.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : String → String → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

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

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

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

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

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

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

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

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