record DomID : Type Utility data type for accessing elements in the DOM.
This will improve type safety and give clearer semantics to a string
that is to be used as an identifier in the DOM.
Totality: total
Visibility: public export
Constructor: D : String -> DomID
Projection: .value : DomID -> String
Hints:
Cast Nat DomID Cast x DomID => Cast (SnocList x) DomID Cast x DomID => Cast (List x) DomID All (\x => Cast (f x) DomID) ks => Cast (All f ks) DomID Eq DomID FromString DomID Interpolation DomID Ord DomID Semigroup DomID Show DomID
.value : DomID -> String- Totality: total
Visibility: public export value : DomID -> String- Totality: total
Visibility: public export toID : Cast t DomID => t -> DomID Alias for `cast` with better type inference.
Totality: total
Visibility: exportwithDomID : Cast t DomID => t -> Node e -> Node e Specialized version of `withId` (which sets the `id` attribute of a
node) for working with `DomID`s.
Totality: total
Visibility: exportforID : Cast t DomID => t -> Attribute x e Set the `for` attribute of a DOM label to the given ID.
Totality: total
Visibility: exporttagRef : (0 tag : HTMLTag s) -> Cast t DomID => t -> Ref tag- Totality: total
Visibility: export elemRef : Cast t DomID => t -> Ref Void- Totality: total
Visibility: export btnRef : Cast t DomID => t -> Ref Button Identifier for accessing a `<button>` element
Totality: total
Visibility: exportdivRef : Cast t DomID => t -> Ref Div Identifier for accessing a `<div>` element
Totality: total
Visibility: exportinpRef : Cast t DomID => t -> Ref Input Identifier for accessing an `<input>` element
Totality: total
Visibility: exportcanvasRef : Cast t DomID => t -> Ref Canvas Identifier for accessing a `<canvas>` element
Totality: total
Visibility: exportref : Cast t DomID => t -> Attribute tag e `id` attribute for a DOM element
Totality: total
Visibility: export