module Agda.Termination.Semiring
( HasZero(..)
, Semiring(..)
, integerSemiring
, intSemiring
, boolSemiring
) where
import Data.Monoid
class Eq a => HasZero a where
zeroElement :: a
data Semiring a = Semiring
{ add :: a -> a -> a
, mul :: a -> a -> a
, zero :: a
}
instance HasZero Integer where
zeroElement = 0
integerSemiring :: Semiring Integer
integerSemiring = Semiring { add = (+), mul = (*), zero = 0 }
instance HasZero Int where
zeroElement = 0
intSemiring :: Semiring Int
intSemiring = Semiring { add = (+), mul = (*), zero = 0 }
boolSemiring :: Semiring Bool
boolSemiring =
Semiring { add = (||), mul = (&&), zero = False }