Type.List

Documentation

data Lst l

type family FromLst a

Equations

FromLst (Lst l) = l

type family Removed el cont :: l

Instances

type Removed [e] e [e] el ((:) e l ls) = If [e] ((==) e el l) ls ((:) e l (Removed [e] e [e] el ls))

type family RemovedIdx idx cont :: l

Instances

type RemovedIdx [k] [k] idx ((:) k l ls) = If [k] ((==) Nat idx 0) ls ((:) k l (RemovedIdx [k] [k] ((-) idx 1) ls))

type family ElAt idx cont :: l

Instances

type ElAt k [k] idx ((:) k l ls) = If k ((==) Nat idx 0) l (ElAt k [k] ((-) idx 1) ls)

type family SuccMaybe m

Equations

SuccMaybe (Just n) = Just (n + 1)

SuccMaybe Nothing = Nothing

data Recursive a

Instances

type Index k * a (Recursive [k1] ([] k1)) = Nothing Nat

type Index k * a (Recursive [k] ((:) k l ls)) = If (Maybe Nat) ((==) k a l) (Just Nat 0) (SuccMaybe (Index k * a (Recursive [k] ls)))

type family Head lst

Equations

Head `[]` = Nothing

Head (a : as) = Just a

type family Head' lst

Equations

Head' (a : as) = a

type family UniqueFix lst

Equations

UniqueFix `[]` = `[]`

UniqueFix lst = Unique lst

type family Reverse' lst lst'

Equations

Reverse' `[]` lst = lst

Reverse' (l : ls) lst = Reverse' ls (l : lst)

type family Take n lst

Equations

Take 0 lst = `[]`

Take n (l : ls) = l : Take (n - 1) ls