Idris2Doc : Web.MVC.Controller.File

Web.MVC.Controller.File

(source)

Definitions

fileC : Cast i DomID => ValEnv i => FileEnv i => i -> Controller FileEv (String, Maybe File)
Totality: total
Visibility: export
file : Cast i DomID => ValEnv i => FileEnv i => Editor i (String, Maybe File) FileEv Body
  Specialized version of `input` for entering file names.

Totality: total
Visibility: export