module Pandora.Paradigm.Primary.Object.Natural where

import Pandora.Pattern.Category (($))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Quasiring (Quasiring (one))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (Ordering (Less, Equal, Greater))

data Natural = Zero | Natural Natural

instance Setoid Natural where
	Natural
Zero == :: Natural -> Natural -> Boolean
== Natural
Zero = Boolean
True
	Natural Natural
n == Natural Natural
m = Natural
n Natural -> Natural -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Natural
m
	Natural
_ == Natural
_ = Boolean
False

instance Chain Natural where
	Natural
Zero <=> :: Natural -> Natural -> Ordering
<=> Natural
Zero = Ordering
Equal
	Natural
Zero <=> Natural Natural
_ = Ordering
Less
	Natural Natural
_ <=> Natural
Zero = Ordering
Greater
	Natural Natural
n <=> Natural Natural
m = Natural
n Natural -> Natural -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> Natural
m

instance Semigroup Natural where
	Natural
Zero + :: Natural -> Natural -> Natural
+ Natural
m = Natural
m
	Natural Natural
n + Natural
m = Natural -> Natural
Natural (Natural -> Natural) -> Natural -> Natural
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Natural
n Natural -> Natural -> Natural
forall a. Semigroup a => a -> a -> a
+ Natural
m

instance Ringoid Natural where
	Natural
Zero * :: Natural -> Natural -> Natural
* Natural
_ = Natural
Zero
	Natural Natural
n * Natural
m = Natural
m Natural -> Natural -> Natural
forall a. Semigroup a => a -> a -> a
+ Natural
n Natural -> Natural -> Natural
forall a. Ringoid a => a -> a -> a
* Natural
m

instance Monoid Natural where
	zero :: Natural
zero = Natural
Zero

instance Quasiring Natural where
	one :: Natural
one = Natural -> Natural
Natural Natural
Zero