Agda-2.4.2.4: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

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 

tests :: IO Bool Source

Tests.