Data.SOP.Utils

Definitions

I : Type -> Type

  Type-level identity function.

Totality: total
Visibility: public export

K : Type -> k -> Type

  Type-level constant function.

Totality: total
Visibility: public export

data SingletonList : List a -> Type

  Witness that a list is actually a singleton list.

Totality: total
Visibility: public export
Constructor: 

IsSingletonList : (v : a) -> SingletonList [v]

Hints:

Uninhabited (SingletonList [])

Uninhabited (SingletonList (a :: (b :: t)))

singletonList : (vs : List a) -> Dec (SingletonList vs)

  Covering function for singleton lists.

Totality: total
Visibility: public export

data UpdateOnce : k -> k -> List k -> List k -> Type

  View for updating a single occurence of a value
  in a list

Totality: total
Visibility: public export
Constructors:

UpdateHere : UpdateOnce t t' (t :: ks) (t' :: ks)

UpdateThere : UpdateOnce t t' ks ks' -> UpdateOnce t t' (k :: ks) (k :: ks')

data UpdateMany : k -> k -> List k -> List k -> Type

  View for updating several occurences of a value
  in a list

Totality: total
Visibility: public export
Constructors:

UMNil : UpdateMany t t' [] []

UMConsSame : UpdateMany t t' ks ks' -> UpdateMany t t' (t :: ks) (t' :: ks')

UMConsDiff : UpdateMany t t' ks ks' -> UpdateMany t t' (k :: ks) (k :: ks')

data Sublist : List k -> List k -> Type

  View of the second List containing all values (in the same order)
  of the first List interleaved with arbitrary additional values.

Totality: total
Visibility: public export
Constructors:

SLNil : Sublist [] ks'

SLSame : Sublist ks ks' -> Sublist (k :: ks) (k :: ks')

SLDiff : Sublist ks ks' -> Sublist ks (k :: ks')

data EnumType : List (List k) -> Type

  Witness that a list of list of types (representing the
  constructors and fields of an ADT) represents an enum type, i.e.
  that all constructors are nullary.

Totality: total
Visibility: public export
Constructors:

EZ : EnumType []

ES : EnumType kss -> EnumType ([] :: kss)

0 enumTail : EnumType (ks :: kss) -> EnumType kss

  If `ks :: kss` is an enum type, then so is `kss`

Totality: total
Visibility: public export

dispStringList : List String -> String

Totality: total
Visibility: export