Agda.Termination.Semiring

Semirings.

Documentation

class 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.

Minimal complete definition

zeroElement

Methods

zeroElement :: a

Instances

HasZero Int

The standard semiring on Ints.

Methods

zeroElement :: Int

HasZero Integer

The standard semiring on Integers.

Methods

zeroElement :: Integer

HasZero Order

Methods

zeroElement :: Order

data Semiring a

Semirings.

Constructors

Semiring

Fields

• add :: a -> a -> a

  Addition.

• mul :: a -> a -> a

  Multiplication.

• zero :: a

  Zero. The one is never used in matrix multiplication , one :: a -- ^ One.

integerSemiring :: Semiring Integer

intSemiring :: Semiring Int

boolSemiring :: Semiring Bool

The standard semiring on Bools.