Camfort.Helpers.Vec

Documentation

data Nat

Constructors

Z

S Nat

data Natural n where

Constructors

Zero :: Natural Z

Succ :: Natural n -> Natural (S n)

Instances

Show (Natural n)

Methods

showsPrec :: Int -> Natural n -> ShowS

show :: Natural n -> String

showList :: [Natural n] -> ShowS

data NatBox where

Constructors

NatBox :: Natural n -> NatBox

Instances

Show NatBox

Methods

showsPrec :: Int -> NatBox -> ShowS

show :: NatBox -> String

showList :: [NatBox] -> ShowS

toNatBox :: Int -> NatBox

class IsNatural n where

Minimal complete definition

fromNat

Methods

fromNat :: Proxy n -> Int

Instances

IsNatural Z

Methods

fromNat :: Proxy Nat Z -> Int

IsNatural n => IsNatural (S n)

Methods

fromNat :: Proxy Nat (S n) -> Int

data Vec n a where

Constructors

Nil :: Vec Z a

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

Instances

Functor (Vec n)

Methods

fmap :: (a -> b) -> Vec n a -> Vec n b

(<$) :: a -> Vec n b -> Vec n a

Foldable (Vec n)

Methods

fold :: Monoid m => Vec n m -> m

foldMap :: Monoid m => (a -> m) -> Vec n a -> m

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

foldr' :: (a -> b -> b) -> b -> Vec n a -> b

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

foldl' :: (b -> a -> b) -> b -> Vec n a -> b

foldr1 :: (a -> a -> a) -> Vec n a -> a

foldl1 :: (a -> a -> a) -> Vec n a -> a

toList :: Vec n a -> [a]

null :: Vec n a -> Bool

length :: Vec n a -> Int

elem :: Eq a => a -> Vec n a -> Bool

maximum :: Ord a => Vec n a -> a

minimum :: Ord a => Vec n a -> a

sum :: Num a => Vec n a -> a

product :: Num a => Vec n a -> a

Eq a => Eq (Vec n a)

Methods

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

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

Ord a => Ord (Vec n a)

Methods

compare :: Vec n a -> Vec n a -> Ordering

(<) :: Vec n a -> Vec n a -> Bool

(<=) :: Vec n a -> Vec n a -> Bool

(>) :: Vec n a -> Vec n a -> Bool

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

max :: Vec n a -> Vec n a -> Vec n a

min :: Vec n a -> Vec n a -> Vec n a

Show a => Show (Vec n a)

Methods

showsPrec :: Int -> Vec n a -> ShowS

show :: Vec n a -> String

showList :: [Vec n a] -> ShowS

length :: Vec n a -> Int

lengthN :: Vec n a -> Natural n

zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c

zip :: Vec n a -> Vec n b -> Vec n (a, b)

findIndex :: (a -> Bool) -> Vec n a -> Maybe Int

(!!) :: Vec n a -> Int -> a

replace :: Int -> a -> Vec n a -> Vec n a

data EqT a b where

Constructors

ReflEq :: EqT a a

data ExistsEqT t n where

Constructors

ExistsEqT :: EqT (t m) n -> ExistsEqT t n

data VecBox a where

Constructors

VecBox :: Vec n a -> VecBox a

fromList :: [a] -> VecBox a

toList :: Vec n a -> [a]

applyListOp :: ([a] -> [a]) -> Vec n a -> Vec n a

Apply length preserving list operation.

proveEqSize :: Vec n a -> Vec m b -> Maybe (EqT m n)

proveNonEmpty :: Vec n a -> Maybe (ExistsEqT S n)

hasSize :: Vec m a -> Natural n -> Maybe (EqT m n)

data VecList a where

Constructors

VL :: [Vec n a] -> VecList a

fromLists :: forall a. [[a]] -> VecList a