Safe Haskell	None
Language	Haskell98

Language.SMTLib2.Internals.Type.List

Documentation

type family Head lst :: a Source

Equations

Head (x : xs) = x

type family Tail lst :: [a] Source

Equations

Tail (x : xs) = xs

type family Index lst idx :: a Source

Equations

Index (x : xs) Z = x
Index (x : xs) (S n) = Index xs n

type family Insert lst idx el :: [a] Source

Equations

Insert (x : xs) Z y = y : xs
Insert (x : xs) (S n) y = x : Insert xs n y

type family Remove lst idx :: [a] Source

Equations

Remove (x : xs) Z = xs
Remove (x : xs) (S n) = x : Remove xs n

type family Append lst el :: [a] Source

Equations

Append `[]` y = y : `[]`
Append (x : xs) y = x : Append xs y

type family Length lst :: Nat Source

Equations

Length `[]` = Z
Length (x : xs) = S (Length xs)

type family Drop lst i :: [a] Source

Equations

Drop lst Z = lst
Drop (x : xs) (S n) = Drop xs n

type family Take lst i :: [a] Source

Equations

Take xs Z = `[]`
Take (x : xs) (S n) = x : Take xs n

type family StripPrefix lst pre :: [a] Source

Equations

StripPrefix xs `[]` = xs
StripPrefix (x : xs) (x : ys) = StripPrefix xs ys

type family Last lst :: a Source

Equations

Last `[x]` = x
Last (x : (y : rest)) = Last (y : rest)

type family DropLast lst :: [a] Source

Equations

DropLast `[x]` = `[]`
DropLast (x : (y : rest)) = x : DropLast (y : rest)

type family Reverse lst :: [a] Source

Equations

Reverse `[]` = `[]`
Reverse (x : xs) = Append (Reverse xs) x

type family Map lst f :: [b] Source

Equations

Map `[]` f = `[]`
Map (x : xs) f = f x : Map xs f

data List e tp where Source

Constructors

Nil :: List e `[]`
(:::) :: e x -> List e xs -> List e (x : xs) infixr 9

Instances

HasMonad (m (List Type e tp)) Source
GCompare k e => GCompare [k] (List k e) Source
GEq k e => GEq [k] (List k e) Source
GShow k e => GShow [k] (List k e) Source
GEq k e => Eq (List k e lst) Source
GCompare k e => Ord (List k e lst) Source
GShow k e => Show (List k e lst) Source
HasMonad (List Type e tp) Source
type MonadResult (m (List Type e tp)) = List Type e tp Source
type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m' Source
type MonadResult (List Type e tp) = List Type e tp Source
type MatchMonad (List Type e tp) m = () Source

list :: [ExpQ] -> ExpQ Source

nil :: List e `[]` Source

list1 :: e t1 -> List e `[t1]` Source

list2 :: e t1 -> e t2 -> List e `[t1, t2]` Source

list3 :: e t1 -> e t2 -> e t3 -> List e `[t1, t2, t3]` Source

reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r Source

access :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e tp)) -> m (a, List e (Insert lst idx tp)) Source

access' :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e (Index lst idx))) -> m (a, List e lst) Source

head :: List e lst -> e (Head lst) Source

tail :: List e lst -> List e (Tail lst) Source

index :: List e lst -> Natural idx -> e (Index lst idx) Source

insert :: List e lst -> Natural idx -> e tp -> List e (Insert lst idx tp) Source

remove :: List e lst -> Natural idx -> List e (Remove lst idx) Source

mapM :: Monad m => (forall x. e x -> m (e' x)) -> List e lst -> m (List e' lst) Source

mapIndexM :: Monad m => (forall n. Natural n -> e (Index lst n) -> m (e' (Index lst n))) -> List e lst -> m (List e' lst) Source

cons :: e x -> List e xs -> List e (x : xs) Source

append :: List e xs -> e x -> List e (Append xs x) Source

length :: List e lst -> Natural (Length lst) Source

drop :: List e lst -> Natural i -> List e (Drop lst i) Source

take :: List e lst -> Natural i -> List e (Take lst i) Source

last :: List e lst -> e (Last lst) Source

dropLast :: List e lst -> List e (DropLast lst) Source

stripPrefix :: GEq e => List e lst -> List e pre -> Maybe (List e (StripPrefix lst pre)) Source

reverse :: List e lst -> List e (Reverse lst) Source

map :: List e lst -> (forall x. e x -> e (f x)) -> List e (Map lst f) Source

unmap :: List p lst -> List e (Map lst f) -> (forall x. e (f x) -> e x) -> List e lst Source

unmapM :: Monad m => List p lst -> List e (Map lst f) -> (forall x. e (f x) -> m (e x)) -> m (List e lst) Source

mapM' :: Monad m => List e lst -> (forall x. e x -> m (e (f x))) -> m (List e (Map lst f)) Source

toList :: Monad m => (forall x. e x -> m a) -> List e lst -> m [a] Source

toListIndex :: Monad m => (forall n. Natural n -> e (Index lst n) -> m a) -> List e lst -> m [a] Source

foldM :: Monad m => (forall x. s -> e x -> m s) -> s -> List e lst -> m s Source

zipWithM :: Monad m => (forall x. e1 x -> e2 x -> m (e3 x)) -> List e1 lst -> List e2 lst -> m (List e3 lst) Source

zipToListM :: Monad m => (forall x. e1 x -> e2 x -> m a) -> List e1 lst -> List e2 lst -> m [a] Source

mapAccumM :: Monad m => (forall x. s -> e x -> m (s, e' x)) -> s -> List e xs -> m (s, List e' xs) Source