smtlib2-1.0: A type-safe interface to communicate with an SMT solver.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Type.Nat

Synopsis

Documentation

data Nat Source #

Natural numbers on the type-level.

Constructors

Z 
S Nat 

Instances

Enum Nat Source # 

Methods

succ :: 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] #

Eq Nat Source # 

Methods

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

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

Integral Nat Source # 

Methods

quot :: 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) #

toInteger :: Nat -> Integer #

Num Nat Source # 

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat Source # 

Methods

compare :: Nat -> Nat -> Ordering #

(<) :: Nat -> Nat -> Bool #

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

(>) :: Nat -> Nat -> Bool #

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

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Real Nat Source # 

Methods

toRational :: Nat -> Rational #

GCompare Nat Natural Source # 

Methods

gcompare :: f a -> f b -> GOrdering Natural a b #

GEq Nat Natural Source # 

Methods

geq :: f a -> f b -> Maybe ((Natural := a) b) #

GShow Nat Natural Source # 

Methods

gshowsPrec :: Int -> t a -> ShowS #

data Natural n where Source #

A concrete representation of the Nat type.

Constructors

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

Instances

GCompare Nat Natural Source # 

Methods

gcompare :: f a -> f b -> GOrdering Natural a b #

GEq Nat Natural Source # 

Methods

geq :: f a -> f b -> Maybe ((Natural := a) b) #

GShow Nat Natural Source # 

Methods

gshowsPrec :: Int -> t a -> ShowS #

Eq (Natural n) Source # 

Methods

(==) :: Natural n -> Natural n -> Bool #

(/=) :: Natural n -> Natural n -> Bool #

Ord (Natural n) Source # 

Methods

compare :: Natural n -> Natural n -> Ordering #

(<) :: Natural n -> Natural n -> Bool #

(<=) :: Natural n -> Natural n -> Bool #

(>) :: Natural n -> Natural n -> Bool #

(>=) :: Natural n -> Natural n -> Bool #

max :: Natural n -> Natural n -> Natural n #

min :: Natural n -> Natural n -> Natural n #

Show (Natural n) Source # 

Methods

showsPrec :: Int -> Natural n -> ShowS #

show :: Natural n -> String #

showList :: [Natural n] -> ShowS #

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

Equations

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

type family (n :: Nat) - (m :: Nat) :: Nat where ... Source #

Equations

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

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

Equations

Z <= m = True 
(S n) <= Z = False 
(S n) <= (S m) = (<=) n m 

naturalToInteger :: Natural n -> Integer Source #

naturalAdd :: Natural n -> Natural m -> Natural (n + m) Source #

naturalSub :: Natural (n + m) -> Natural n -> Natural m Source #

naturalSub' :: Natural n -> Natural m -> (forall diff. (m + diff) ~ n => Natural diff -> a) -> a Source #

naturalLEQ :: Natural n -> Natural m -> Maybe (Dict ((n <= m) ~ True)) Source #

reifyNat :: Nat -> (forall n. Natural n -> r) -> r Source #

Get a static representation for a dynamically created natural number.

Example:

>>> reifyNat (S (S Z)) show
"2"

5) :: Natural ('S ('S ('S ('S ('S 'Z)))))

nat :: (Num a, Ord a) => a -> ExpQ Source #

natT :: (Num a, Ord a) => a -> TypeQ Source #

A template haskell function to create nicer looking number types.

Example:

>>> $(nat 5) :: Natural $(natT 5)
5

type N0 = Z Source #

type N1 = S N0 Source #

type N2 = S N1 Source #

type N3 = S N2 Source #

type N4 = S N3 Source #

type N5 = S N4 Source #

type N6 = S N5 Source #

type N7 = S N6 Source #

type N8 = S N7 Source #

type N9 = S N8 Source #

type N10 = S N9 Source #

type N11 = S N10 Source #

type N12 = S N11 Source #

type N13 = S N12 Source #

type N14 = S N13 Source #

type N15 = S N14 Source #

type N16 = S N15 Source #

type N17 = S N16 Source #

type N18 = S N17 Source #

type N19 = S N18 Source #

type N20 = S N19 Source #

type N21 = S N20 Source #

type N22 = S N21 Source #

type N23 = S N22 Source #

type N24 = S N23 Source #

type N25 = S N24 Source #

type N26 = S N25 Source #

type N27 = S N26 Source #

type N28 = S N27 Source #

type N29 = S N28 Source #

type N30 = S N29 Source #

type N31 = S N30 Source #

type N32 = S N31 Source #

type N33 = S N32 Source #

type N34 = S N33 Source #

type N35 = S N34 Source #

type N36 = S N35 Source #

type N37 = S N36 Source #

type N38 = S N37 Source #

type N39 = S N38 Source #

type N40 = S N39 Source #

type N41 = S N40 Source #

type N42 = S N41 Source #

type N43 = S N42 Source #

type N44 = S N43 Source #

type N45 = S N44 Source #

type N46 = S N45 Source #

type N47 = S N46 Source #

type N48 = S N47 Source #

type N49 = S N48 Source #

type N50 = S N49 Source #

type N51 = S N50 Source #

type N52 = S N51 Source #

type N53 = S N52 Source #

type N54 = S N53 Source #

type N55 = S N54 Source #

type N56 = S N55 Source #

type N57 = S N56 Source #

type N58 = S N57 Source #

type N59 = S N58 Source #

type N60 = S N59 Source #

type N61 = S N60 Source #

type N62 = S N61 Source #

type N63 = S N62 Source #

type N64 = S N63 Source #

class IsNatural n where Source #

Minimal complete definition

getNatural

Methods

getNatural :: Natural n Source #

Instances

deriveIsNatural :: Natural n -> Dict (IsNatural n) Source #