inductive Lean.Html : Type

HTML content, which may be either a single node or a sequence of sibling nodes.

This type is optimized for convenient authoring of HTML documents. It is not formally related to the HTML DOM representation. It is analogous to React's Fragment.

• element (tag : String) (attrs : Array (String × String)) (children : Html) : Html

  An element with the given tag name, attributes, and children.

• text : String → Html

  Textual content.

  The characters &, <, and > are always escaped to HTML entities during rendering. Use raw in raw text elements (script and style) instead.

• raw : String → Html

  Characters to be copied verbatim (and not escaped) during rendering.

• seq : Array Html → Html

  A sequence of HTML values.

partial def Lean.instReprHtml.repr : Html → Nat → Format

@[instance_reducible]

instance Lean.instReprHtml : Repr Html

Equations

• Lean.instReprHtml = { reprPrec := Lean.instReprHtml.repr }

@[instance_reducible]

instance Lean.instInhabitedHtml : Inhabited Html

Equations

• Lean.instInhabitedHtml = { default := Lean.instInhabitedHtml.default }

@[instance_reducible]

instance Lean.instBEqHtml : BEq Html

Equations

• Lean.instBEqHtml = { beq := Lean.instBEqHtml.beq }

partial def Lean.instBEqHtml.beq : Html → Html → Bool

partial def Lean.instHashableHtml.hash : Html → UInt64

@[instance_reducible]

instance Lean.instHashableHtml : Hashable Html

Equations

• Lean.instHashableHtml = { hash := Lean.instHashableHtml.hash }

@[instance_reducible]

instance Lean.instTypeNameHtml : TypeName Html

Equations

• Lean.instTypeNameHtml = Lean.inst✝

partial def Lean.instToExprHtml.toExpr : Html → Expr

@[instance_reducible]

instance Lean.instToExprHtml : ToExpr Html

Equations

• Lean.instToExprHtml = { toExpr := Lean.instToExprHtml.toExpr, toTypeExpr := Lean.Expr.const `Lean.Html [] }

def Lean.Html.empty : Html

Empty HTML.

Equations

• Lean.Html.empty = Lean.Html.seq #[]

@[irreducible]

def Lean.Html.isEmpty : Html → Bool

Whether this HTML is rendered as the empty string.

Equations

• (Lean.Html.seq a).isEmpty = a.attach.all fun (x : { x : Lean.Html // x ∈ a }) => match x with | ⟨h, property⟩ => h.isEmpty
• (Lean.Html.text s).isEmpty = s.isEmpty
• (Lean.Html.raw s).isEmpty = s.isEmpty
• (Lean.Html.element tag attrs children).isEmpty = false

def Lean.Html.ofString (escape : Bool) : String → Html

If escape is true, then characters such as & are escaped to entities such as & during rendering.

Use false in raw text elements (script and style).

Equations

• Lean.Html.ofString escape = if escape = true then Lean.Html.text else Lean.Html.raw

@[instance_reducible]

instance Lean.Html.instCoeString : Coe String Html

Equations

• Lean.Html.instCoeString = { coe := Lean.Html.text }

def Lean.Html.append : Html → Html → Html

Appends two HTML forests.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Html.seq xs).append x✝ = if xs.isEmpty = true then x✝ else Lean.Html.seq (xs.push x✝)
• x✝.append (Lean.Html.seq ys) = if ys.isEmpty = true then x✝ else Lean.Html.seq (#[x✝] ++ ys)
• x✝¹.append x✝ = Lean.Html.seq #[x✝¹, x✝]

@[instance_reducible]

instance Lean.Html.instAppend : Append Html

Equations

• Lean.Html.instAppend = { append := Lean.Html.append }

def Lean.Html.ofCollection {ρ : Type w} [ForIn Id ρ Html] (hs : ρ) : Html

Merges a collection of HTML values by appending them.

Like seq (ForIn.toArray hs), but may produce a more compact representation.

Equations

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

def Lean.Html.ofArray (hs : Array Html) : Html

Merges an array of HTML values by appending them.

Like seq, but may produce a more compact representation.

Equations

• Lean.Html.ofArray hs = Lean.Html.ofCollection hs

def Lean.Html.ofList (hs : List Html) : Html

Merges a list of HTML values by appending them.

Like seq hs.toArray, but may produce a more compact representation.

Equations

• Lean.Html.ofList hs = Lean.Html.ofCollection hs

def Lean.Html.ofOption (h? : Option Html) : Html

Returns the given HTML, or empty when the input is none.

Equations

• Lean.Html.ofOption h? = h?.getD Lean.Html.empty

@[instance_reducible]

instance Lean.Html.instCoeArray : Coe (Array Html) Html

Equations

• Lean.Html.instCoeArray = { coe := Lean.Html.ofArray }

@[instance_reducible]

instance Lean.Html.instCoeList : Coe (List Html) Html

Equations

• Lean.Html.instCoeList = { coe := Lean.Html.ofList }

@[instance_reducible]

instance Lean.Html.instCoeOption : Coe (Option Html) Html

Equations

• Lean.Html.instCoeOption = { coe := Lean.Html.ofOption }

@[instance_reducible]

instance Lean.Html.instToJson : ToJson Html

A compact JSON encoding of Html.

Equations

• Lean.Html.instToJson = { toJson := Lean.Html.instToJson.to }

@[irreducible]

def Lean.Html.instToJson.to : Html → Json

Equations

• One or more equations did not get rendered due to their size.
• Lean.Html.instToJson.to (Lean.Html.text t) = Lean.Json.str t
• Lean.Html.instToJson.to (Lean.Html.raw r) = Lean.Json.mkObj [("r", Lean.toJson r)]
• Lean.Html.instToJson.to (Lean.Html.seq hs) = Lean.Json.arr (Array.map Lean.Html.instToJson.to hs)

@[instance_reducible]

instance Lean.Html.instFromJson : FromJson Html

Equations

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

partial def Lean.Html.instFromJson.from? : Json → Except String Html

@[instance_reducible]

instance Lean.Html.instQuoteMkStr1 : Quote Html

Equations

• Lean.Html.instQuoteMkStr1 = { quote := Lean.Html.instQuoteMkStr1.q }

partial def Lean.Html.instQuoteMkStr1.q : Html → TSyntax `term

partial def Lean.Html.rewritePostM {m : Type → Type u_1} [Monad m] (fn : Html → m Html) : Html → m Html

Rewrites the forest by using fn to transform every node. Traversal proceeds in post-order: fn receives element and seq nodes with already-rewritten children.

def Lean.Html.rewritePost (fn : Html → Html) (h : Html) : Html

Rewrites the forest by using fn to transform every node. Traversal proceeds in post-order: fn receives element and seq nodes with already-rewritten children.

Equations

• Lean.Html.rewritePost fn h = (Lean.Html.rewritePostM fn h).run