Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data PeanoNat
- addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
- type family Add a b where ...
- subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
- multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
- peanoToNatural :: PeanoNat -> Natural
- naturalToPeano :: Natural -> PeanoNat
- type family PeanoToNatural pn where ...
- type family ListLength l where ...
Documentation
Inductive natural numbers.
Instances
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat Source #
subtractFromPeanoNat a b = b - a
peanoToNatural :: PeanoNat -> Natural Source #
naturalToPeano :: Natural -> PeanoNat Source #
type family PeanoToNatural pn where ... Source #
PeanoToNatural 'Zero = 0 | |
PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1 |
type family ListLength l where ... Source #
ListLength '[] = 'Zero | |
ListLength (a ': aa) = 'Succ (ListLength aa) |