Safe Haskell	Safe-Inferred
Language	Haskell2010

Pipeline.Internal.Common.Nat

Synopsis

data Nat
- = Zero
- | Succ Nat
data SNat (n :: Nat) where
- SZero :: SNat 'Zero
- SSucc :: SNat n -> SNat ('Succ n)
type N1 = 'Succ 'Zero
type N2 = 'Succ N1
type N3 = 'Succ N2
type N4 = 'Succ N3
type N5 = 'Succ N4
type N6 = 'Succ N5
type N7 = 'Succ N6
type N8 = 'Succ N7
type N9 = 'Succ N8
type family (m :: Nat) := (n :: Nat) :: Bool where ...
type family (a :: Nat) :+ (b :: Nat) where ...
class IsNat (n :: Nat) where
- nat :: SNat n

Documentation

data Nat #

Datatype for representing natural numbers

Constructors

Zero	Natural number for 0
Succ Nat	Natural number for n + 1

Instances

Instances details

BuildNetworkAlg BasicNetwork Map #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Map (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Task #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Task (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork DropR #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). DropR (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork DropL #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). DropL (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Swap #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Swap (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Beside #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Beside (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Then #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Then (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Replicate #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Replicate (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
BuildNetworkAlg BasicNetwork Id #
Instance details Defined in Pipeline.Internal.Backend.BasicNetwork Methods buildNetworkAlg :: forall (asS :: [Type -> Type]) (asT :: [Type]) (bsS :: [Type -> Type]) (bsT :: [Type]) (csS :: [Type -> Type]) (csT :: [Type]) (nbs :: k). Id (N BasicNetwork asS asT) bsS bsT csS csT nbs -> IO (N BasicNetwork asS asT bsS bsT csS csT nbs) #
IFunctor5 Map #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Map f' a b c d e -> Map g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Map f' a b c d e -> m (Map g' a b c d e) #
IFunctor5 Task #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Task f' a b c d e -> Task g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Task f' a b c d e -> m (Task g' a b c d e) #
IFunctor5 DropR #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> DropR f' a b c d e -> DropR g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> DropR f' a b c d e -> m (DropR g' a b c d e) #
IFunctor5 DropL #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> DropL f' a b c d e -> DropL g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> DropL f' a b c d e -> m (DropL g' a b c d e) #
IFunctor5 Swap #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Swap f' a b c d e -> Swap g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Swap f' a b c d e -> m (Swap g' a b c d e) #
IFunctor5 Beside #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Beside f' a b c d e -> Beside g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Beside f' a b c d e -> m (Beside g' a b c d e) #
IFunctor5 Then #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Then f' a b c d e -> Then g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Then f' a b c d e -> m (Then g' a b c d e) #
IFunctor5 Replicate #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Replicate f' a b c d e -> Replicate g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Replicate f' a b c d e -> m (Replicate g' a b c d e) #
IFunctor5 Id #
Instance details Defined in Pipeline.Internal.Core.CircuitAST Methods imap5 :: forall f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> g' a b c d e) -> Id f' a b c d e -> Id g' a b c d e # imapM5 :: forall m f' g' (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). Monad m => (forall (a :: k) (b :: k) (c :: k) (d :: k) (e :: k). f' a b c d e -> m (g' a b c d e)) -> Id f' a b c d e -> m (Id g' a b c d e) #

data SNat (n :: Nat) where #

Constructors

SZero :: SNat 'Zero
SSucc :: SNat n -> SNat ('Succ n)

type N1 = 'Succ 'Zero #

Nat equal to 1

type N2 = 'Succ N1 #

Nat equal to 2

type N3 = 'Succ N2 #

Nat equal to 3

type N4 = 'Succ N3 #

Nat equal to 4

type N5 = 'Succ N4 #

Nat equal to 5

type N6 = 'Succ N5 #

Nat equal to 6

type N7 = 'Succ N6 #

Nat equal to 7

type N8 = 'Succ N7 #

Nat equal to 8

type N9 = 'Succ N8 #

Nat equal to 9

type family (m :: Nat) := (n :: Nat) :: Bool where ... #

Equations

('Succ n) := 'Zero = 'False
'Zero := 'Zero = 'True
'Zero := ('Succ n) = 'False
('Succ m) := ('Succ n) = m := n

type family (a :: Nat) :+ (b :: Nat) where ... #

Equations

a :+ 'Zero = a
a :+ ('Succ b) = 'Succ (a :+ b)

class IsNat (n :: Nat) where #

Methods

nat :: SNat n #

Instances

Instances details

IsNat 'Zero #
Instance details Defined in Pipeline.Internal.Common.Nat Methods nat :: SNat 'Zero #
IsNat n => IsNat ('Succ n) #
Instance details Defined in Pipeline.Internal.Common.Nat Methods nat :: SNat ('Succ n) #