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

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Type.Nat

Documentation

data Nat Source

Constructors

Z 
S Nat 

Instances

data Natural n where Source

Constructors

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

Instances

type family n + m :: Nat Source

Equations

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

type family n - m :: Nat Source

Equations

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

type family n <= m :: Bool 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

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

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

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