Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
A singleton
-esque type for representing Peano natural numbers.
- data Nat :: N -> * where
- _Z :: Z :~: Z
- _S :: (x :~: y) -> S x :~: S y
- _s :: (S x :~: S y) -> x :~: y
- _ZneS :: (Z :~: S x) -> Void
- addZ :: Nat x -> (x + Z) :~: x
- addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
- (.+) :: Nat x -> Nat y -> Nat (x + y)
- (.*) :: Nat x -> Nat y -> Nat (x * y)
- (.^) :: Nat x -> Nat y -> Nat (x ^ y)
- nat :: Nat n -> Int
- n0 :: Nat N0
- n1 :: Nat N1
- n2 :: Nat N2
- n3 :: Nat N3
- n4 :: Nat N4
- n5 :: Nat N5
- n6 :: Nat N6
- n7 :: Nat N7
- n8 :: Nat N8
- n9 :: Nat N9
- n10 :: Nat N10
Documentation
data Nat :: N -> * where Source
TestEquality N Nat Source | |
DecEquality N Nat Source | |
Known N Nat Z Source | |
Known N Nat n => Known N Nat (S n) Source | If |
Witness ØC (Known N Nat n) (Nat n) Source | A |
Witness ØC (Known N Nat n) (VT k n f a) Source | |
Eq (Nat n) Source | |
Ord (Nat n) Source | |
Show (Nat n) Source | |
type KnownC N Nat Z = ØC | |
type KnownC N Nat (S n) = Known N Nat n Source | |
type WitnessC ØC (Known N Nat n) (Nat n) = ØC | |
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC |