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

Agda.Termination.Semiring

Description

Semirings.

Synopsis

# Documentation

class Eq a => HasZero a where Source #

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

Instances

 Source # The standard semiring on Ints. Methods Source # The standard semiring on Integers. Methods Source # Methods

class (Eq a, Monoid a) => SemiRing a where Source #

SemiRing type class. Additive monoid with multiplication operation. Inherit addition and zero from Monoid.

Minimal complete definition

multiply

Methods

multiply :: a -> a -> a Source #

data Semiring a Source #

Semirings.

Constructors

 Semiring Fieldsadd :: a -> a -> aAddition.mul :: a -> a -> aMultiplication.zero :: aZero. The one is never used in matrix multiplication , one :: a -- ^ One.

semiringInvariant :: Eq a => Semiring a -> a -> a -> a -> Bool Source #

Semiring invariant.

The standard semiring on Bools.