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

Safe Haskell | Safe-Infered

Agda.Utils.SemiRing

# Documentation

class SemiRing a where

Methods

oplus :: a -> a -> a

otimes :: a -> a -> a

Instances

SemiRing E |
SemiRing Distance |
SemiRing Weight |
SemiRing Occurrence | `Occurrence` is a complete lattice with least element `Mixed` and greatest element `Unused`. It forms a commutative semiring where `oplus` is meet (glb) and `otimes` is composition. Both operations are idempotent. For `oplus`, `Unused` is neutral (zero) and `Mixed` is dominant. For `otimes`, `StrictPos` is neutral (one) and `Unused` is dominant.
SemiRing Edge | These operations form a semiring if we quotient by the relation "the `Occurrence` components are equal".
SemiRing a => SemiRing (Maybe a) |