Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Termination.Semiring
Description
Semirings.
Synopsis
class Eq a => HasZero a where
zeroElement :: a
class (Eq a, Monoid a) => SemiRing a where
multiply :: a -> a -> a
data Semiring a = Semiring {
add :: a -> a -> a
mul :: a -> a -> a
zero :: a
}
semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> Bool
integerSemiring :: Semiring Integer
boolSemiring :: Semiring Bool
tests :: IO Bool
Documentation
class Eq a => HasZero a whereSource
HasZero is needed for sparse matrices, to tell which is the element that does not have to be stored. It is a cut-down version of SemiRing which is definable without the implicit ?cutoff.
Methods
zeroElement :: aSource
class (Eq a, Monoid a) => SemiRing a whereSource
SemiRing type class. Additive monoid with multiplication operation. Inherit addition and zero from Monoid.
Methods
multiply :: a -> a -> aSource
data Semiring a Source
Semirings.
Constructors
Semiring
add :: a -> a -> aAddition.
mul :: a -> a -> aMultiplication.
zero :: aZero. The one is never used in matrix multiplication , one :: a -- ^ One.
semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> BoolSource
Semiring invariant.
integerSemiring :: Semiring IntegerSource
boolSemiring :: Semiring BoolSource
The standard semiring on Bools.
tests :: IO BoolSource
Produced by Haddock version 2.6.1