Longboi

Documentation

data Nat

Constructors

Z

S Nat

Instances

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

type family (n :: Nat) + (m :: Nat) :: Nat where ... infixl 6

Equations

Z + m = m

(S n) + m = S (n + m)

type family (n :: Nat) * (m :: Nat) :: Nat where ... infixl 7

Equations

Z * m = Z

(S n) * m = (n * m) + m

type family (n :: Nat) - (m :: Nat) :: Nat where ... infixl 6

Equations

Z - m = Z

(S n) - Z = S n

(S n) - m = S (n - m)

type family Min (n :: Nat) (m :: Nat) :: Nat where ...

Equations

Min Z Z = Z

Min Z (S m) = Z

Min (S n) Z = Z

Min (S n) (S m) = S (Min n m)

type family Max (n :: Nat) (m :: Nat) :: Nat where ...

Equations

Max Z Z = Z

Max Z (S m) = S m

Max (S n) Z = S n

Max (S n) (S m) = S (Max n m)

data Longboi a (n :: Nat) where

Constructors

Nil :: Longboi a Z

Cons :: a -> Longboi a n -> Longboi a (S n)

Instances

Eq a => Eq (Longboi a n)

Methods

(==) :: Longboi a n -> Longboi a n -> Bool

(/=) :: Longboi a n -> Longboi a n -> Bool

type family Length (xs :: Longboi a (n :: Nat)) :: Nat where ...

Equations

Length Nil = Z

Length (Cons x xs) = S Z + Length xs

type family Contains (xs :: Longboi a (n :: Nat)) (elem :: a) :: Bool where ...

Equations

Contains Nil _ = False

Contains (Cons x xs) x = True

Contains (Cons x xs) y = Contains xs y

(++) :: Longboi a n -> Longboi a m -> Longboi a (n + m) infixr 5

type family Append (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (m :: Nat)) :: Longboi a (n + m) where ...

Equations

Append (Cons x xs) ys = Cons x (Append xs ys)

Append Nil ys = ys

type family Head (xs :: Longboi a (n :: Nat)) :: a where ...

Equations

Head (Cons x _) = x

type family Last (xs :: Longboi a (n :: Nat)) :: a where ...

Equations

Last (Cons x Nil) = x

Last (Cons x xs) = Last xs

type family Tail (xs :: Longboi a (S n :: Nat)) :: Longboi a (n :: Nat) where ...

Equations

Tail (Cons _ xs) = xs

type family Init (xs :: Longboi a (S n :: Nat)) :: Longboi a (n :: Nat) where ...

Equations

Init (Cons _ Nil) = Nil

Init (Cons x xs) = Cons x (Init xs)

type family Null (xs :: Longboi a (n :: Nat)) :: Bool where ...

Equations

Null Nil = True

Null _ = False

type family VMap (f :: a -> b) (xs :: Longboi a (n :: Nat)) :: Longboi b (n :: Nat) where ...

Equations

VMap _ Nil = Nil

VMap f (Cons x xs) = Cons (f x) (VMap f xs)

type family Foldl (f :: a -> b -> a) (x :: a) (ys :: Longboi b (n :: Nat)) :: a where ...

Equations

Foldl _ x Nil = x

Foldl f y (Cons x xs) = Foldl f (f y x) xs

type family Foldr (f :: a -> b -> b) (x :: b) (ys :: Longboi a (n :: Nat)) :: b where ...

Equations

Foldr _ y Nil = y

Foldr f y (Cons x xs) = f x (Foldr f y xs)

type family ZipWithSame (f :: a -> b -> c) (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (n :: Nat)) :: Longboi c (n :: Nat) where ...

Equations

ZipWithSame _ Nil Nil = Nil

ZipWithSame f (Cons a as) (Cons b bs) = Cons (f a b) (ZipWithSame f as bs)

type family ZipWith (f :: a -> b -> c) (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (m :: Nat)) :: Longboi c (Min n m) where ...

Equations

ZipWith _ Nil Nil = Nil

ZipWith _ Nil (Cons _ _) = Nil

ZipWith _ (Cons _ _) Nil = Nil

ZipWith f (Cons a as) (Cons b bs) = Cons (f a b) (ZipWith f as bs)

head :: Longboi a (S n) -> a

last :: Longboi a n -> a

tail :: Longboi a (S n) -> Longboi a n

init :: Longboi a (S n) -> Longboi a n

uncons :: Longboi a (S n) -> (a, Longboi a n)

null :: Longboi a n -> Bool

vmap :: (a -> b) -> Longboi a n -> Longboi b n

foldl :: (a -> b -> a) -> a -> Longboi b n -> a

foldr :: (a -> b -> b) -> b -> Longboi a n -> b

toList :: Longboi a n -> [a]

zipWithSame :: (a -> b -> c) -> Longboi a n -> Longboi b n -> Longboi c n

zipWith :: (a -> b -> c) -> Longboi a n -> Longboi b m -> Longboi c (Min n m)