Data.Functor.Naperian

Definitions

interface Naperian : (Type -> Type) -> Type

Parameters: f
Constraints: Applicative f
Methods:

Log : Type

lookup : f a -> Log -> a

tabulate : (Log -> a) -> f a

Implementations:

Naperian (Vect n)

Naperian f => Naperian g => Naperian (g . f)

Log : Naperian f => Type

Totality: total
Visibility: public export

lookup : {auto __con : Naperian f} -> f a -> Log -> a

Totality: total
Visibility: public export

tabulate : {auto __con : Naperian f} -> (Log -> a) -> f a

Totality: total
Visibility: public export

positions : {auto {conArg:4925} : Naperian f} -> f Log

Totality: total
Visibility: public export

transpose : Naperian f => Naperian g => f (g a) -> g (f a)

Totality: total
Visibility: public export