Algebra.Semiring

Definitions

interface Semiring : Type -> Type

  A Semiring has two binary operations and an identity for each

Parameters: a
Methods:

(|+|) : a -> a -> a

Fixity Declaration: infixl operator, level 8

plusNeutral : a

(|*|) : a -> a -> a

Fixity Declaration: infixl operator, level 9

timesNeutral : a

Implementation: 

Semiring ZeroOneOmega

(|+|) : Semiring a => a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

plusNeutral : Semiring a => a

Totality: total
Visibility: public export

(|*|) : Semiring a => a -> a -> a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

timesNeutral : Semiring a => a

Totality: total
Visibility: public export

erased : Semiring a => a

  Erased linearity corresponds to the neutral for |+|

Totality: total
Visibility: public export

linear : Semiring a => a

  Purely linear corresponds to the neutral for |*|

Totality: total
Visibility: public export

elimSemi : (Semiring a, Eq a) => b -> b -> (a -> b) -> a -> b

  A semiring eliminator

Totality: total
Visibility: public export

isErased : (Semiring a, Eq a) => a -> Bool

Totality: total
Visibility: export

isLinear : (Semiring a, Eq a) => a -> Bool

Totality: total
Visibility: export

isRigOther : (Semiring a, Eq a) => a -> Bool

Totality: total
Visibility: export

branchZero : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b

Totality: total
Visibility: export

branchOne : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b

Totality: total
Visibility: export

branchVal : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b

Totality: total
Visibility: export