Language.SMTLib2.Internals.Type.Nat

Documentation

data Nat

Natural numbers on the type-level.

Constructors

Z

S Nat

Instances

Enum Nat

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

Methods

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

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

Integral Nat

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

Methods

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

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

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

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

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

Methods

toRational :: Nat -> Rational

GCompare Nat Natural

Methods

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

GEq Nat Natural

Methods

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

GShow Nat Natural

Methods

gshowsPrec :: Int -> t a -> ShowS

data Natural n where

A concrete representation of the Nat type.

Constructors

Zero :: Natural Z

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

Instances

GCompare Nat Natural

Methods

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

GEq Nat Natural

Methods

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

GShow Nat Natural

Methods

gshowsPrec :: Int -> t a -> ShowS

Eq (Natural n)

Methods

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

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

Ord (Natural n)

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)

Methods

showsPrec :: Int -> Natural n -> ShowS

show :: Natural n -> String

showList :: [Natural n] -> ShowS

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

Equations

Z + n = n

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

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

Equations

n - Z = n

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

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

Equations

Z <= m = True

(S n) <= Z = False

(S n) <= (S m) = (<=) n m

naturalToInteger :: Natural n -> Integer

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

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

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

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

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

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

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

A template haskell function to create nicer looking number types.

Example:

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

type N0 = Z

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9

type N11 = S N10

type N12 = S N11

type N13 = S N12

type N14 = S N13

type N15 = S N14

type N16 = S N15

type N17 = S N16

type N18 = S N17

type N19 = S N18

type N20 = S N19

type N21 = S N20

type N22 = S N21

type N23 = S N22

type N24 = S N23

type N25 = S N24

type N26 = S N25

type N27 = S N26

type N28 = S N27

type N29 = S N28

type N30 = S N29

type N31 = S N30

type N32 = S N31

type N33 = S N32

type N34 = S N33

type N35 = S N34

type N36 = S N35

type N37 = S N36

type N38 = S N37

type N39 = S N38

type N40 = S N39

type N41 = S N40

type N42 = S N41

type N43 = S N42

type N44 = S N43

type N45 = S N44

type N46 = S N45

type N47 = S N46

type N48 = S N47

type N49 = S N48

type N50 = S N49

type N51 = S N50

type N52 = S N51

type N53 = S N52

type N54 = S N53

type N55 = S N54

type N56 = S N55

type N57 = S N56

type N58 = S N57

type N59 = S N58

type N60 = S N59

type N61 = S N60

type N62 = S N61

type N63 = S N62

type N64 = S N63

class IsNatural n where

Minimal complete definition

getNatural

Methods

getNatural :: Natural n

Instances

IsNatural Z

Methods

getNatural :: Natural Z

IsNatural n => IsNatural (S n)

Methods

getNatural :: Natural (S n)

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