Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.Termination.Semiring

Description

Semirings.

Synopsis

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

Instances

HasZero Integer

The standard semiring on Integers.

HasZero Order 

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

Instances

data Semiring a Source

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.

semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> BoolSource

Semiring invariant.

boolSemiring :: Semiring BoolSource

The standard semiring on Bools.