Idris2Doc : Data.W

Data.W(source)

Definitions
data Fin : Type
  Totality: total
  Visibility: public export
  Constructors:
  
AVoid : Fin
  
AUnit : String -> Fin
  
(||) : Fin -> Fin -> Fin
fromString : String -> Fin
  Totality: total
  Visibility: public export
data NamedUnit : String -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkNamedUnit : NamedUnit nm
Elem : Fin -> Type
  Totality: total
  Visibility: public export
lookup : (d : Fin) -> String -> Maybe (Elem d)
  Totality: total
  Visibility: public export
record Shape : Fin -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkShape : Elem d -> Shape d

  Projection: 
.runShape : Shape d -> Elem d
fromString : (nm : String) -> IsJust (lookup d nm) => Shape d
  Totality: total
  Visibility: public export
record One : String -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkOne : s -> One nm s

  Projection: 
.runOne : One nm s -> s
.runOne : One nm s -> s
  Totality: total
  Visibility: public export
runOne : One nm s -> s
  Totality: total
  Visibility: public export
Arr : Fin -> Type -> Type
  Totality: total
  Visibility: public export
record (~>) : Fin -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkArr : Arr d r -> d ~> r

  Projection: 
.runArr : d ~> r -> Arr d r

  Fixity Declarations:
  infixr operator, level 0
infixr operator, level 0
.runArr : d ~> r -> Arr d r
  Totality: total
  Visibility: public export
runArr : d ~> r -> Arr d r
  Totality: total
  Visibility: public export
(.=) : (nm : String) -> s -> One nm s
  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 5
lamArr : (d : Fin) -> (Elem d -> r) -> Arr d r
  Totality: total
  Visibility: public export
appArr : (d : Fin) -> Arr d r -> Elem d -> r
  Totality: total
  Visibility: public export
($$) : d ~> r -> Elem d -> r
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
PiArr : (d : Fin) -> Arr d Type -> Type
  Totality: total
  Visibility: public export
lam : ((x : Elem d) -> b $$ x) -> Pi d b
  Totality: total
  Visibility: export
appArr : (d : Fin) -> PiArr d b -> (x : Elem d) -> appArr d b x
  Totality: total
  Visibility: public export
($$) : Pi d b -> (x : Elem d) -> b $$ x
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 0
beta : (f : ((x : Elem d) -> b $$ x)) -> (x : Elem d) -> lam f $$ x = f x
  Totality: total
  Visibility: export
eta : (f : Pi d b) -> lam (\x => f $$ x) = f
  Totality: total
  Visibility: export
ext : (f : ((x : Elem d) -> b $$ x)) -> (g : ((x : Elem d) -> b $$ x)) -> ((x : Elem d) -> f x = g x) -> lam f = lam g
  Totality: total
  Visibility: export
cases : PiArr d (lamArr d (b . MkShape)) -> (x : Shape d) -> b x
  Totality: total
  Visibility: public export
NAT : Type
  Totality: total
  Visibility: public export
mkPSet : (d : Fin) -> Arr d Type -> PSet
  Totality: total
  Visibility: public export
lamArr : (d : Fin) -> (e : Arr d Type) -> (k : Arr d e Type) -> ((x : ElemArr d e) -> appArr d e k x) -> PiArr d e k
  Totality: total
  Visibility: public export
lam : ((x : Elem p) -> k $$ x) -> Pi p k
  Totality: total
  Visibility: public export
appArr : (d : Fin) -> (e : Arr d Type) -> (k : Arr d e Type) -> PiArr d e k -> (x : ElemArr d e) -> appArr d e k x
  Totality: total
  Visibility: public export
($$) : Pi p k -> (x : Elem p) -> k $$ x
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 0
data W : (sh : Type) -> (sh -> PSet) -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkW : (s : sh) -> pos s ~> W sh pos -> W sh pos