Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Termination.Semiring

Description

Semirings.

Synopsis

class Eq a => HasZero a where zeroElement :: a class (Eq a, Monoid a) => SemiRing a where multiply :: a -> a -> a data Semiring a = Semiring { add :: a -> a -> a mul :: a -> a -> a zero :: a } semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> Bool integerSemiring :: Semiring Integer boolSemiring :: Semiring Bool tests :: IO Bool

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. Methods zeroElement :: a Source

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

SemiRing type class. Additive monoid with multiplication operation. Inherit addition and zero from Monoid. Methods multiply :: a -> a -> a Source

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

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

Semiring invariant.

integerSemiring :: Semiring Integer Source

boolSemiring :: Semiring Bool Source

The standard semiring on Bools.

tests :: IO Bool Source

Produced by Haddock version 2.6.1