natural-induction 0.1.1.0 → 0.2.0.0

raw patch · 2 files changed

+8/−4 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Natural/Class.hs +7/−3
• natural-induction.cabal +1/−1

@@ -1,5 +1,6 @@ module Data.Natural.Class where +import Prelude hiding (iterate) import Data.Functor.Const import Data.Peano import Data.Proxy@@ -13,6 +14,9 @@ instance Natural n => Natural (Succ n) where     natural _ sf = sf -reify :: Natural n => Proxy n -> Peano-reify (Proxy :: Proxy n) = getConst $ natural @n (Const Zero) (φ $ Const . Succ . reify)-  where φ = ($ Proxy) :: ∀ f a . (Proxy a -> f a) -> f a+reify :: Natural n => Const Peano n+reify = iterate Succ Zero++iterate :: ∀ n a . Natural n => (a -> a) -> a -> Const a n+iterate f a = natural (Const a) (f' (iterate f a))+  where f' = Const . f . getConst :: ∀ n . Const a n -> Const a (Succ n)

@@ -1,5 +1,5 @@ name:                natural-induction-version:             0.1.1.0+version:             0.2.0.0 synopsis:            Induction over natural numbers -- description:          license:             BSD3