Structures.Dependent.DList

Definitions

data DList : (value_type : Type) -> (value_type -> Type) -> List value_type -> Type

  Collects dependently typed values indexed by `value_type`, with type 
  constructor `elem_type`, into a single collection by collecting a list of 
  `value_types` at the type level in the `values` list.

Totality: total
Visibility: public export
Constructors:

Nil : DList value_type elem_type []

(::) : elem_type x -> DList value_type elem_type xs -> DList value_type elem_type (x :: xs)

data NonEmpty : DList value_type elem_type values -> Type

Totality: total
Visibility: public export
Constructor: 

IsNonEmpty : NonEmpty (x :: xs)

data Empty : DList value_type elem_type values -> Type

Totality: total
Visibility: public export
Constructor: 

IsEmpty : Empty []

head : (xs : DList value_type elem_type (value :: values)) -> NonEmpty xs => elem_type value

Visibility: public export

tail : (xs : DList value_type elem_type (value :: values)) -> NonEmpty xs => DList value_type elem_type values

Visibility: public export

HeadType : Maybe value_type -> (value_type -> Type) -> Type

Visibility: public export

listTail : List x -> Maybe (List x)

Visibility: public export

TailType : Maybe (List value_type) -> (value_type -> Type) -> Type

Visibility: public export

head' : DList value_type elem_type values -> HeadType (head' values) elem_type

Visibility: public export

tail' : DList value_type elem_type values -> TailType (listTail values) elem_type

Visibility: public export

length : DList value_type elem_type values -> Nat

Visibility: public export

take : (n : Nat) -> DList value_type elem_type values -> DList value_type elem_type (take n values)

Visibility: public export

drop : (n : Nat) -> DList value_type elem_type values -> DList value_type elem_type (drop n values)

Visibility: public export

(++) : DList value_type elem_type values_1 -> DList value_type elem_type values_2 -> DList value_type elem_type (values_1 ++ values_2)

Visibility: public export
Fixity Declaration: infixr operator, level 7

dFind : ((v : value_type) -> elem_type v -> Bool) -> DList value_type elem_type values -> Maybe (v : value_type ** elem_type v)

  Find the first element satisfying the given predicate 

Visibility: export

dDelete : ((v : value_type) -> elem_type v -> Bool) -> DList value_type elem_type values -> (vs : List value_type ** DList value_type elem_type vs)

  Delete the first element satisfying the given predicate

Visibility: export

dDeleteAll : ((v : value_type) -> elem_type v -> Bool) -> DList value_type elem_type values -> (vs : List value_type ** DList value_type elem_type vs)

  Delete the first element satisfying the gicen predicate 

Visibility: export

dFilter : ((v : value_type) -> elem_type v -> Bool) -> DList value_type elem_type values -> (values' : List value_type ** DList value_type elem_type values')

  Keep only the elements that satisfy the given predicate

Visibility: export

dMap : ((v : value_type) -> elem_type v -> x) -> DList value_type elem_type values -> List x

Visibility: export

dMap' : ((v : value_type) -> elem_type v -> (v' : value_type' ** elem_type' v')) -> DList value_type elem_type values -> (values' : List value_type' ** DList value_type' elem_type' values')

Visibility: export

dFoldL : (acc -> (v : value_type) -> elem_type v -> acc) -> acc -> DList value_type elem_type values -> acc

Visibility: export

toList : DList value_type elem_type values -> List (v : value_type ** elem_type v)

Visibility: public export

fromList : List (v : value_type ** elem_type v) -> (values : List value_type ** DList value_type elem_type values)

Visibility: public export

($==) : DecEq value_type => ((v : value_type) -> Eq (elem_type v)) => DList value_type elem_type vs1 -> DList value_type elem_type vs2 -> Bool

Visibility: export
Fixity Declaration: infix operator, level 6

data PList : (value_type : Type) -> (value_type -> Type) -> (pred_type : (value_type -> Type)) -> (values : List value_type) -> DList value_type pred_type values -> Type

Totality: total
Visibility: public export
Constructors:

Nil : PList value_type elem_type pred_type values proofs

(::) : elem_type value -> {auto prf : pred_type value} -> PList value_type elem_type pred_type values proofs -> PList value_type elem_type pred_type (value :: values) (prf :: proofs)