Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Positivity.Occurrence

Description

Occurrences.

Synopsis

Documentation

data Occurrence Source

Subterm occurrences for positivity checking. The constructors are listed in increasing information they provide: Mixed <= JustPos <= StrictPos <= GuardPos <= Unused Mixed <= JustNeg <= Unused.

Constructors

Mixed	Arbitrary occurrence (positive and negative).
JustNeg	Negative occurrence.
JustPos	Positive occurrence, but not strictly positive.
StrictPos	Strictly positive occurrence.
GuardPos	Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records.
Unused

Instances

Bounded Occurrence Source
Enum Occurrence Source
Eq Occurrence Source
Ord Occurrence Source
Show Occurrence Source
NFData Occurrence Source
StarSemiRing Occurrence 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.
CoArbitrary Occurrence Source
Arbitrary Occurrence Source
Null Occurrence Source
KillRange Occurrence Source
PrettyTCM Occurrence Source
EmbPrj Occurrence Source
Abstract [Occurrence] Source
Apply [Occurrence] Source
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source

prop_Occurrence_oplus_associative :: Occurrence -> Occurrence -> Occurrence -> Bool Source

prop_Occurrence_oplus_ozero :: Occurrence -> Bool Source

prop_Occurrence_oplus_commutative :: Occurrence -> Occurrence -> Bool Source

prop_Occurrence_otimes_associative :: Occurrence -> Occurrence -> Occurrence -> Bool Source

prop_Occurrence_otimes_oone :: Occurrence -> Bool Source

prop_Occurrence_distributive :: Occurrence -> Occurrence -> Occurrence -> Bool Source

prop_Occurrence_otimes_ozero :: Occurrence -> Bool Source

prop_Occurrence_ostar :: Occurrence -> Bool Source

tests :: IO Bool Source

Tests.