Data.Fun.Nary

Definitions

data Visibility : Type

Totality: total
Visibility: public export
Constructors:

Visible : Visibility

Hidden : Visibility

Auto : Visibility

Pi : Visibility -> (a : Type) -> (a -> Type) -> Type

Totality: total
Visibility: public export

lam : (vis : Visibility) -> (0 b : (a -> Type)) -> ((x : a) -> b x) -> Pi vis a b

Totality: total
Visibility: public export

app : (vis : Visibility) -> (0 b : (a -> Type)) -> Pi vis a b -> (x : a) -> b x

Totality: total
Visibility: public export

PI : (n : Nat) -> Visibility -> (a : Type) -> (Vect n a -> Type) -> Type

Totality: total
Visibility: public export

curry : (n : Nat) -> (vis : Visibility) -> (0 b : (Vect n a -> Type)) -> ((as : Vect n a) -> b as) -> PI n vis a b

Totality: total
Visibility: public export

uncurry : (n : Nat) -> (vis : Visibility) -> (0 b : (Vect n a -> Type)) -> PI n vis a b -> (as : Vect n a) -> b as

Totality: total
Visibility: public export