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

@[instance_reducible]

instance Lean.instInhabitedHtml : Inhabited Html

@[instance_reducible]

instance Lean.instBEqHtml : BEq Html

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

partial def Lean.instHashableHtml.hash : Html → UInt64

@[instance_reducible]

instance Lean.instHashableHtml : Hashable Html

@[instance_reducible]

instance Lean.instTypeNameHtml : TypeName Html

partial def Lean.instToExprHtml.toExpr : Html → Expr

@[instance_reducible]

instance Lean.instToExprHtml : ToExpr Html

def Lean.Html.empty : Html

Empty HTML.

@[irreducible]

def Lean.Html.isEmpty : Html → Bool

Whether this HTML is rendered as the empty string.

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

@[instance_reducible]

instance Lean.Html.instCoeString : Coe String Html

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

Appends two HTML forests.

@[instance_reducible]

instance Lean.Html.instAppend : Append Html

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.

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.

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.

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance Lean.Html.instToJson : ToJson Html

A compact JSON encoding of Html.

@[irreducible]

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

@[instance_reducible]

instance Lean.Html.instFromJson : FromJson Html

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

@[instance_reducible]

instance Lean.Html.instQuoteMkStr1 : Quote Html

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.