Safe Haskell	None
Language	Haskell2010

Agda.Utils.SemiRing

Synopsis

class SemiRing a where
- ozero :: a
- oone :: a
- oplus :: a -> a -> a
- otimes :: a -> a -> a
class SemiRing a => StarSemiRing a where
- ostar :: a -> a

Documentation

class SemiRing a where Source #

Methods

oplus :: a -> a -> a Source #

otimes :: a -> a -> a Source #

Instances details

SemiRing Occurrence Source #	`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.
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source #
SemiRing () Source #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: () Source # oone :: () Source # oplus :: () -> () -> () Source # otimes :: () -> () -> () Source #
Monoid a => SemiRing (Edge a) Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ozero :: Edge a Source # oone :: Edge a Source # oplus :: Edge a -> Edge a -> Edge a Source # otimes :: Edge a -> Edge a -> Edge a Source #
SemiRing a => SemiRing (Maybe a) Source #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: Maybe a Source # oone :: Maybe a Source # oplus :: Maybe a -> Maybe a -> Maybe a Source # otimes :: Maybe a -> Maybe a -> Maybe a Source #

Methods

Instances details

StarSemiRing Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence Source #
StarSemiRing () Source #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: () -> () Source #
StarSemiRing a => StarSemiRing (Maybe a) Source #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: Maybe a -> Maybe a Source #