Semirings (https://en.wikipedia.org/wiki/Semiring).
Instances5SemiRing
SemiRing OccurrenceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity.OccurrenceOccurrence 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 WeightDefined in Agda-2.7.0.1 · Agda.Utils.WarshallSemiRing ()Defined in Agda-2.7.0.1 · Agda.Utils.SemiRingSemiRing (Edge (Seq OccursWhere))Defined in Agda-2.7.0.1 · Agda.TypeChecking.PositivityThese operations form a semiring if we quotient by the relation "the Occurrence components are equal".
SemiRing a => SemiRing (Maybe a)Defined in Agda-2.7.0.1 · Agda.Utils.SemiRing