Data.W

Definitions

fromString : String -> Fin

Totality: total
Visibility: public export

fromString : (nm : String) -> IsJust (lookup d nm) => Shape d

Totality: total
Visibility: 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

NAT : Type

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