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
- pred' :: Nat (S x) -> Nat x
- onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)
- _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)
- elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n
- natVal :: Nat n -> Int
Documentation
data Nat :: N -> * where Source #
TestEquality N Nat Source # | |
Read1 N Nat Source # | |
Show1 N Nat Source # | |
Ord1 N Nat Source # | |
Eq1 N Nat Source # | |
BoolEquality N Nat Source # | |
Known N Nat Z Source # | |
Known N Nat n => Known N Nat (S n) Source # | If |
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
Witness ØC (Known N Nat n) (Nat n) Source # | A |
Witness ØC (Known N Nat n) (VecT k n f a) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source # | |
Eq (Nat n) Source # | |
Ord (Nat n) Source # | |
Show (Nat n) Source # | |
type KnownC N Nat Z Source # | |
type KnownC N Nat (S n) Source # | |
type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
type WitnessC ØC (Known N Nat n) (Nat n) Source # | |
type WitnessC ØC (Known N Nat n) (VecT k n f a) Source # | |
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source # | |
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source # | |
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source # | |