Web.Async.List

Definitions

data ListEv : Type

Totality: total
Visibility: public export
Constructors:

Prepend : ListEv

Append : ListEv

Hints:

Eq ListEv

Ord ListEv

Show ListEv

editList : {default 4294967294 _ : Nat} -> Act (Ref Void, HTMLNodes -> Widget ListEv) -> (HTMLNodes -> Act (Ref Void, Widget ())) -> Editor t -> Editor (List t)

  An editor for lists of values.
  
  This uses `row` to wrap a node for editing a single value
  in a node with some kind of *delete* or *remove* function.
  
  All rows are displayed in the `parent` node.

Totality: total
Visibility: export

editList1 : Editor (List t) -> Editor (List1 t)

  Like `editList` but for non-empty lists.

Totality: total
Visibility: export