type-level-natural-number-operations (empty) → 1.0

raw patch · 4 files changed

+72/−0 lines, 4 filesdep +basedep +type-level-natural-numbersetup-changed

Dependencies added: base, type-level-natural-number

Files

• LICENSE +22/−0
• Setup.hs +2/−0
• TypeLevel/NaturalNumber/Operations.hs +27/−0
• type-level-natural-number-operations.cabal +21/−0

@@ -0,0 +1,22 @@+Copyright (c) 2010, Gregory M. Crosswhite+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.++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,27 @@+{- Copyright (c) 2010, Gregory M. Crosswhite. All rights reserved. -}++{-# LANGUAGE TypeFamilies #-}++module TypeLevel.NaturalNumber.Operations where++import TypeLevel.NaturalNumber++-- | The 'Plus' type family provides a function that adds two+-- type-level natural numbers.  This function is implemented by+-- induction on the first argument --- a fact that one should be aware+-- of when using it in function signatures.+type family Plus m n+-- | base case+type instance Plus Zero n = n+-- | inductive case+type instance Plus (SuccessorTo m) n = SuccessorTo (Plus m n)++-- | The 'Plus' type family provides a function that subtracts two+-- type-level natural numbers.  This function is implemented by+-- induction on both arguments, with the base case being when the+-- second argument is Zero.+type family Minus m n+-- | base case+type instance Minus m Zero = m+-- | inductive case+type instance Minus (SuccessorTo m) (SuccessorTo n) = Minus m n

@@ -0,0 +1,21 @@+Name:                type-level-natural-number-operations+Version:             1.0+License:             BSD3+License-file:        LICENSE+Author:              Gregory Crosswhite+Maintainer:          Gregory Crosswhite <gcross@phys.washington.edu>+Stability:           Provisional+Synopsis:            Basic operations on type-level natural numbers.+Description:         This package provides some basic operations that do not+		     require the UndecideableInstances extension on type-level+		     natural numbers.  Specifically, this package provides the+		     Plus and Minus type functions.+Cabal-version:       >=1.2.3+Build-type:          Simple+Category:	     Type System,Data++Library+    Build-depends:   base >= 3 && < 5,+                     type-level-natural-number >= 1.0 && < 1.2+    Exposed-modules: TypeLevel.NaturalNumber.Operations+    Extensions:	     TypeFamilies