Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.SemiRing

Synopsis

Documentation

class SemiRing a where Source #

Methods

ozero :: a Source #

oone :: a Source #

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

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

Instances

Instances details
SemiRing () Source # 
Instance details

Defined in Agda.Utils.SemiRing

Methods

ozero :: () Source #

oone :: () Source #

oplus :: () -> () -> () Source #

otimes :: () -> () -> () Source #

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

SemiRing Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

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 #

SemiRing (Edge (Seq OccursWhere)) Source #

These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

Instance details

Defined in Agda.TypeChecking.Positivity

class SemiRing a => StarSemiRing a where Source #

Methods

ostar :: a -> a Source #

Instances

Instances details
StarSemiRing () Source # 
Instance details

Defined in Agda.Utils.SemiRing

Methods

ostar :: () -> () Source #

StarSemiRing Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

StarSemiRing a => StarSemiRing (Maybe a) Source # 
Instance details

Defined in Agda.Utils.SemiRing

Methods

ostar :: Maybe a -> Maybe a Source #