Web.MVC.Controller.Form

Definitions

data Editors : Type -> List Type -> List Type -> List Type -> Type

  A heterogeneous list of editors.
  
  These can be used to create UI forms from single - but
  arbitrarily complex - widgets.

Totality: total
Visibility: public export
Constructors:

Nil : Editors i [] [] []

(::) : Editor i s e n -> Editors i ss es ns -> Editors i (s :: ss) (e :: es) (n :: ns)

toProgs : Editors i ss es ns -> i -> Progs es ss

  Converts a list of editors to a list of controllers.

Visibility: public export

toInit : Editors i ss es ns -> i -> HList ss -> Cmd (HSum es)

  Initial commands from a list of editors and a heterogeneous list of
  initial states.

Visibility: export

form : (List (Node (HSum es)) -> Node (HSum es)) -> Editors i ss es ns -> Editor i (HList ss) (HSum es) (HList ns)

  Converts a heterogeneous list of editors into a single editor,
  similar in concept to a form of widgets.

Visibility: export