class Texify (α : Type u) : Type u

• texify : α → String
• requiresParentheses : Bool

  If further constructions that make use of this should add parentheses around it

def texify {α : Type u} [Texify α] : α → String

Equations

• texify = Texify.texify

def texifyWithBrackets {α : Type u} [Texify α] (x : α) : String

Equations

• texifyWithBrackets x = toString "{" ++ toString (texify x) ++ toString "}"

def texifyWithBracketsAndParenthesesIfNecessary {α : Type u} [Texify α] (x : α) : String

Equations

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

def texifyToMd {α : Type u} [Texify α] (a : α) : String

Equations

• texifyToMd a = toString "$$" ++ toString (texify a) ++ toString "$$"

def displayMd (md : String) (stx : Lean.Syntax) : Lean.CoreM Unit

Equations

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

unsafe def evalStringUnsafe (stx : Lean.Term) : Lean.Elab.TermElabM String

Equations

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

@[implemented_by evalStringUnsafe]

opaque evalString : Lean.Term → Lean.Elab.TermElabM String

Evaluates a term of type ProofWidgets.Html

def «command#texify_» : Lean.ParserDescr

Equations

• «command#texify_» = Lean.ParserDescr.node `«command#texify_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#texify") (Lean.ParserDescr.cat `term 0))

@[implicit_reducible]

instance instTexifyNat : Texify Nat

Equations

• instTexifyNat = { texify := fun (n : Nat) => toString n, requiresParentheses := false }

@[implicit_reducible]

instance instTexifyInt : Texify Int

Equations

• instTexifyInt = { texify := fun (n : Int) => toString n, requiresParentheses := false }