Agda-2.5.2.20170816: A dependently typed functional programming language and proof assistant
Agda.Termination.Semiring
Description
Semirings.
Synopsis
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.
HasZero
SemiRing
?cutoff
Minimal complete definition
zeroElement
Methods
zeroElement :: a Source #
Instances
The standard semiring on Ints.
Int
zeroElement :: Int Source #
The standard semiring on Integers.
Integer
zeroElement :: Integer Source #
zeroElement :: Order Source #
data Semiring a Source #
Constructors
Fields
Addition.
Multiplication.
Zero. The one is never used in matrix multiplication , one :: a -- ^ One.
integerSemiring :: Semiring Integer Source #
intSemiring :: Semiring Int Source #
boolSemiring :: Semiring Bool Source #
The standard semiring on Bools.
Bool