natural-induction 0.1.0.1 → 0.1.1.0

raw patch · 2 files changed

+21/−1 lines, 2 files

Files

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

@@ -0,0 +1,18 @@+module Data.Natural.Class where++import Data.Functor.Const+import Data.Peano+import Data.Proxy++class Natural n where+    natural :: f Zero -> (∀ m . Natural m => f (Succ m)) -> f n++instance Natural Zero where+    natural zf _ = zf++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

@@ -1,5 +1,5 @@ name:                natural-induction-version:             0.1.0.1+version:             0.1.1.0 synopsis:            Induction over natural numbers -- description:          license:             BSD3@@ -19,6 +19,8 @@   -- hs-source-dirs:         default-language:    Haskell2010   default-extensions:  UnicodeSyntax+                     , ScopedTypeVariables+                     , TypeApplications                      , RankNTypes                      , PolyKinds                      , DataKinds