packages feed

type-natural 0.0.2.1 → 0.0.3.0

raw patch · 2 files changed

+31/−3 lines, 2 filesdep +template-haskellPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: template-haskell

API changes (from Hackage documentation)

+ Data.Type.Natural: nat :: QuasiQuoter
+ Data.Type.Natural: snat :: QuasiQuoter
- Data.Type.Natural: (%:*) :: Sing t_a3ZC -> forall (t_a3ZD :: Nat). Sing t_a3ZD -> Sing (:* t_a3ZC t_a3ZD)
+ Data.Type.Natural: (%:*) :: Sing t_a42x -> Sing t_a42y -> Sing (:* t_a42x t_a42y)
- Data.Type.Natural: (%:+) :: Sing t_a3Zy -> forall (t_a3Zz :: Nat). Sing t_a3Zz -> Sing (:+ t_a3Zy t_a3Zz)
+ Data.Type.Natural: (%:+) :: Sing t_a42t -> Sing t_a42u -> Sing (:+ t_a42t t_a42u)
- Data.Type.Natural: (%:-) :: Sing t_a3ZA -> forall (t_a3ZB :: Nat). Sing t_a3ZB -> Sing (:- t_a3ZA t_a3ZB)
+ Data.Type.Natural: (%:-) :: Sing t_a42v -> Sing t_a42w -> Sing (:- t_a42v t_a42w)
- Data.Type.Natural: (%:<<=) :: Sing t_a4Bt -> forall (t_a4Bu :: Nat). Sing t_a4Bu -> Sing (:<<= t_a4Bt t_a4Bu)
+ Data.Type.Natural: (%:<<=) :: Sing t_a4E9 -> Sing t_a4Ea -> Sing (:<<= t_a4E9 t_a4Ea)
- Data.Type.Natural: sMax :: Sing t_a3O5 -> forall (t_a3O6 :: Nat). Sing t_a3O6 -> Sing (Max t_a3O5 t_a3O6)
+ Data.Type.Natural: sMax :: Sing t_a3R8 -> Sing t_a3R9 -> Sing (Max t_a3R8 t_a3R9)
- Data.Type.Natural: sMin :: Sing t_a3O3 -> forall (t_a3O4 :: Nat). Sing t_a3O4 -> Sing (Min t_a3O3 t_a3O4)
+ Data.Type.Natural: sMin :: Sing t_a3R6 -> Sing t_a3R7 -> Sing (Min t_a3R6 t_a3R7)
- Data.Type.Natural: sS :: Sing n_a3xp -> Sing (S n_a3xp)
+ Data.Type.Natural: sS :: Sing n_a3As -> Sing (S n_a3As)
- Data.Type.Natural: type SNat (a_a3xo :: Nat) = Sing a_a3xo
+ Data.Type.Natural: type SNat (a_a3Ar :: Nat) = Sing a_a3Ar

Files

Data/Type/Natural.hs view
@@ -12,7 +12,7 @@                      SNat, Sing (SZ, SS)                     -- ** Smart constructors                     , sZ, sS-                    -- ** Arithmetic functions and thir singletons.+                    -- ** Arithmetic functions and their singletons.                     , min, Min, sMin, max, Max, sMax                     , (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*)                     , (:-:), (:-), (%:-), (%-)@@ -22,6 +22,8 @@                     , LeqTrueInstance(..), propToBoolLeq                     -- * Conversion functions                     , natToInt, intToNat, sNatToInt+                    -- * Quasi quotes for natural numbers+                    , nat, snat                     -- * Properties of natural numbers                     , succCongEq, plusCongR, plusCongL, succPlusL, succPlusR                     , plusZR, plusZL, eqPreservesS, plusAssociative@@ -50,7 +52,8 @@                                    Show (..), error, id, otherwise, ($), (.), undefined) import qualified Prelude          as P import           Proof.Equational-+import Language.Haskell.TH.Quote+import Language.Haskell.TH  -------------------------------------------------- -- * Natural numbers and its singleton type@@ -637,3 +640,27 @@       | n < 0     = error "negative integer!"       | n == 0    = Monomorphic sZ       | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn++--------------------------------------------------+-- * Quasi Quoter+--------------------------------------------------++-- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.+--+--   for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@+nat :: QuasiQuoter+nat = QuasiQuoter { quoteExp = P.foldr appE (conE 'Z) . P.flip P.replicate (conE 'S) . P.read+                  , quotePat = P.foldr (\a b -> conP a [b]) (conP 'Z []) . P.flip P.replicate 'S . P.read+                  , quoteType = P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read+                  , quoteDec = error "not implemented"+                  }++-- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.+-- +--  For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@+snat :: QuasiQuoter+snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read+                   , quotePat = P.foldr (\a b -> conP a [b]) (conP 'SZ []) . P.flip P.replicate 'SS . P.read+                   , quoteType = appT (conT ''SNat) . P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read+                   , quoteDec = error "not implemented"+                   }
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.0.2.1+version:             0.0.3.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural@@ -26,3 +26,4 @@                ,       singletons               == 0.8.*                ,       equational-reasoning     == 0.0.*                ,       monomorphic              >= 0.0.3+               ,       template-haskell         == 2.8.*