Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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 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 () Source # 
Instance details

Defined in Agda.Utils.SemiRing

Methods

ozero :: () Source #

oone :: () Source #

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

otimes :: () -> () -> () 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

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 #

class SemiRing a => StarSemiRing a where Source #

Methods

ostar :: a -> a Source #

Instances

Instances details
StarSemiRing Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

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 #