type-indexed-queues-0.1.0.1: Queues with verified and unverified versions.

TypeLevel.Nat

Description

Type-level Peano arithmetic.

Synopsis

# Documentation

>>> import Test.QuickCheck
>>> :{
instance Arbitrary Nat where
arbitrary = fmap (fromInteger . getNonNegative) arbitrary
:}


data Nat Source #

Peano numbers. Care is taken to make operations as lazy as possible:

>>> 1 > S (S undefined)
False
>>> Z > undefined
False
>>> 3 + (undefined :: Nat) >= 3
True


Constructors

 Z S Nat

Instances

 Source # The maximum bound here is infinity.(maxBound :: Nat) > n Methods Source # Uses custom enumFrom, enumFromThen, enumFromThenTo to avoid expensive conversions to and from Int.>>> [1..3] :: [Nat] [1,2,3] >>> [1..1] :: [Nat] [1] >>> [2..1] :: [Nat] [] >>> take 3 [1,2..] :: [Nat] [1,2,3] >>> take 3 [5,4..] :: [Nat] [5,4,3] >>> [1,3..7] :: [Nat] [1,3,5,7] >>> [5,4..1] :: [Nat] [5,4,3,2,1] >>> [5,3..1] :: [Nat] [5,3,1]  Methodssucc :: Nat -> Nat #pred :: Nat -> Nat #toEnum :: Int -> Nat #fromEnum :: Nat -> Int #enumFrom :: Nat -> [Nat] #enumFromThen :: Nat -> Nat -> [Nat] #enumFromTo :: Nat -> Nat -> [Nat] #enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] # Source # Methods(==) :: Nat -> Nat -> Bool #(/=) :: Nat -> Nat -> Bool # Source # Not at all optimized.>>> 5 div 2 :: Nat 2  Methodsquot :: Nat -> Nat -> Nat #rem :: Nat -> Nat -> Nat #div :: Nat -> Nat -> Nat #mod :: Nat -> Nat -> Nat #quotRem :: Nat -> Nat -> (Nat, Nat) #divMod :: Nat -> Nat -> (Nat, Nat) # Source # Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat #dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Nat) #dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) #gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat # Source # Subtraction stops at zero.n >= m ==> m - n == Z Methods(+) :: Nat -> Nat -> Nat #(-) :: Nat -> Nat -> Nat #(*) :: Nat -> Nat -> Nat #negate :: Nat -> Nat #abs :: Nat -> Nat #signum :: Nat -> Nat # Source # As lazy as possible Methodscompare :: Nat -> Nat -> Ordering #(<) :: Nat -> Nat -> Bool #(<=) :: Nat -> Nat -> Bool #(>) :: Nat -> Nat -> Bool #(>=) :: Nat -> Nat -> Bool #max :: Nat -> Nat -> Nat #min :: Nat -> Nat -> Nat # Source # Reads the integer representation. Methods Source # Reasonably expensive. Methods Source # Shows integer representation. MethodsshowsPrec :: Int -> Nat -> ShowS #show :: Nat -> String #showList :: [Nat] -> ShowS # Source # Associated Typestype Rep Nat :: * -> * # Methodsfrom :: Nat -> Rep Nat x #to :: Rep Nat x -> Nat # Source # Will obviously diverge for values like maxBound. Methodsrnf :: Nat -> () # type Rep Nat Source # type Rep Nat = D1 (MetaData "Nat" "TypeLevel.Nat" "type-indexed-queues-0.1.0.1-GPaLldpmb1Q20PpM0x8M72" False) ((:+:) (C1 (MetaCons "Z" PrefixI False) U1) (C1 (MetaCons "S" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat)))) data The Nat Source # Singleton for type-level Peano numbers. data The Nat whereZy :: The Nat ZSy :: The Nat (S n)

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