singleton-nats (empty) → 0.1.0.0

raw patch · 4 files changed

+103/−0 lines, 4 filesdep +basedep +singletonssetup-changed

Dependencies added: base, singletons

Files

• Data/Nat.hs +48/−0
• LICENSE +30/−0
• Setup.hs +2/−0
• singleton-nats.cabal +23/−0

@@ -0,0 +1,48 @@+{-# LANGUAGE+  UndecidableInstances, ScopedTypeVariables, DataKinds,+  FlexibleInstances, GADTs, TypeFamilies, TemplateHaskell,+  TypeOperators #-}++module Data.Nat (+    Nat(..)+  , (Data.Nat.+)+  , (Data.Nat.*)+  , SNat+  , (:*)+  , (:*$)+  , (:*$$)+  , (:+)    +  , (:+$)+  , (:+$$)+  , SSym0(..)+  , SSym1(..)+  , ZSym0(..)+  , (%:+)+  , (%:*)+  , Lit+  , SLit ) where++import Data.Singletons.TH+import Data.Singletons.Prelude+import qualified GHC.TypeLits as Lit++$(singletons [d|+  data Nat = Z | S Nat deriving (Eq, Show, Ord)++  (+) :: Nat -> Nat -> Nat+  Z + b = b+  S a + b = S (a + b)++  (*) :: Nat -> Nat -> Nat+  Z * b = Z+  S a * b = b + (a * b) |])++type family Lit n where+  Lit 0 = Z+  Lit n = S (Lit (n Lit.- 1))++type SLit n = Sing (Lit n)++++

@@ -0,0 +1,30 @@+Copyright (c) 2015, András Kovács++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of András Kovács nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,23 @@++name:                singleton-nats+version:             0.1.0.0+synopsis:            Unary natural numbers relying on the singletons infrastructure.         +license:             BSD3+license-file:        LICENSE+author:              András Kovács+maintainer:          puttamalac@gmail.com+copyright:           2015 András Kovács+category:            Data+build-type:          Simple++cabal-version:       >=1.10++library+  exposed-modules:+    Data.Nat++  build-depends:       +    base >=4.7 && <4.9,+    singletons >= 1++  default-language:    Haskell2010