ModuleAgda-2.8.0.2Haskell2010

Agda.Termination.Semiring

Semirings.

Synopsis

class HasZero
data Semiring
value integerSemiring
value intSemiring
value boolSemiring

PackageAgda-2.8.0.2
Exports5
LanguageHaskell2010
LicenceMIT
SourceSemiring.hs

classclass Eq a => HasZero a where

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 :: a

Instances3HasZero

HasZero OrderDefined in Agda-2.8.0.2 · Agda.Termination.Order
HasZero IntegerDefined in Agda-2.8.0.2 · Agda.Termination.Semiring
The standard semiring on Integers.
HasZero IntDefined in Agda-2.8.0.2 · Agda.Termination.Semiring
The standard semiring on Ints.

datadata Semiring a

Source#

Semirings.

Constructors

Semiring
- add :: a -> a -> a
  Addition.
- mul :: a -> a -> a
  Multiplication.
- zero :: a
  Zero. The one is never used in matrix multiplication , one :: a -- ^ One.

valueintegerSemiring :: Semiring Integer

valueintSemiring :: Semiring Int

valueboolSemiring :: Semiring Bool

Source#

The standard semiring on Bools.