| Copyright | Copyright (c) 2014 Kenneth Foner |
|---|---|
| Maintainer | kenneth.foner@gmail.com |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Numeric.Witness.Peano
Description
This module defines GADT type witnesses for Peano-style natural numbers.
- data Zero
- data Succ n
- data Natural n where
- class ReifyNatural n where
- reifyNatural :: Natural n
- type family LessThanOrEqual a b
- type (<=) a b = LessThanOrEqual a b ~ True
- type family LessThan a b
- type (<) a b = LessThan a b ~ True
- type family x + y
- type family x - y
- plus :: Natural a -> Natural b -> Natural (a + b)
- minus :: b <= a => Natural a -> Natural b -> Natural (a - b)
Documentation
Instances
Instances
| ReifyNatural n => ReifyNatural (Succ n) |
Natural numbers paired with type-level natural numbers. These terms act as witnesses of a particular natural.
class ReifyNatural n where Source
Given a context expecting a particular natural, we can manufacture it from the aether.
Methods
reifyNatural :: Natural n Source
Instances
| ReifyNatural Zero | |
| ReifyNatural n => ReifyNatural (Succ n) |
type family LessThanOrEqual a b Source
Type level less-than-or-equal test.
Equations
| LessThanOrEqual Zero Zero = True | |
| LessThanOrEqual Zero (Succ m) = True | |
| LessThanOrEqual (Succ n) (Succ m) = LessThanOrEqual n m | |
| LessThanOrEqual x y = False |
type (<=) a b = LessThanOrEqual a b ~ True Source
This constraint is a more succinct way of requiring that a be less than or equal to b.
type (<) a b = LessThan a b ~ True Source
This constraint is a more succinct way of requiring that a be less than b.