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.Simproc

Equations

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

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

Equations

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