natural-induction-0.2.0.0: Induction over natural numbers
Data.Natural.Class
class Natural n where Source #
Minimal complete definition
natural
Methods
natural :: f Zero -> (forall m. Natural m => f (Succ m)) -> f n Source #
Instances
natural :: f Zero -> (forall m. Natural m => f (Succ m)) -> f Zero Source #
natural :: f Zero -> (forall m. Natural m => f (Succ m)) -> f (Succ n) Source #
reify :: Natural n => Const Peano n Source #
iterate :: forall n a. Natural n => (a -> a) -> a -> Const a n Source #