Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Utils.SemiRing
Documentation
class SemiRing a where Source #
Semirings (https://en.wikipedia.org/wiki/Semiring).
Methods
Instances
SemiRing Occurrence Source # |
It forms a commutative semiring where For |
Defined in Agda.TypeChecking.Positivity.Occurrence Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source # | |
SemiRing Weight Source # | |
SemiRing () Source # | |
SemiRing (Edge (Seq OccursWhere)) Source # | These operations form a semiring if we quotient by the relation
"the |
Defined in Agda.TypeChecking.Positivity Methods ozero :: Edge (Seq OccursWhere) Source # oone :: Edge (Seq OccursWhere) Source # oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source # otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source # | |
SemiRing a => SemiRing (Maybe a) Source # | |
class SemiRing a => StarSemiRing a where Source #
Star semirings (https://en.wikipedia.org/wiki/Semiring#Star_semirings).
Instances
StarSemiRing Occurrence Source # | |
Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence Source # | |
StarSemiRing () Source # | |
Defined in Agda.Utils.SemiRing | |
StarSemiRing a => StarSemiRing (Maybe a) Source # | |
Defined in Agda.Utils.SemiRing |