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

Safe HaskellNone

Agda.TypeChecking.Irrelevance

Contents

Description

Irrelevant function types.

Synopsis

Documentation

unusableRelevance :: Relevance -> BoolSource

unusableRelevance rel == True iff we cannot use a variable of rel.

composeRelevance :: Relevance -> Relevance -> RelevanceSource

Relevance composition. Irrelevant is dominant, Relevant is neutral.

inverseComposeRelevance :: Relevance -> Relevance -> RelevanceSource

inverseComposeRelevance r x returns the most irrelevant y such that forall x, y we have x `moreRelevant` (r `composeRelevance` y) iff (r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).

ignoreForced :: Relevance -> RelevanceSource

For comparing Relevance ignoring Forced and UnusedArg.

irrToNonStrict :: Relevance -> RelevanceSource

Irrelevant function arguments may appear non-strictly in the codomain type.

Operations on Dom.

hideAndRelParams :: Dom a -> Dom aSource

Prepare parts of a parameter telescope for abstraction in constructors and projections.

inverseApplyRelevance :: Relevance -> Dom a -> Dom aSource

Used to modify context when going into a rel argument.

applyRelevance :: Relevance -> Dom a -> Dom aSource

Compose two relevance flags. This function is used to update the relevance information on pattern variables a after a match against something rel.

Operations on Context.

workOnTypes :: TCM a -> TCM aSource

Modify the context whenever going from the l.h.s. (term side) of the typing judgement to the r.h.s. (type side).

doWorkOnTypes :: TCM a -> TCM aSource

Call me if --experimental-irrelevance is set.

workOnTypes' :: Bool -> TCM a -> TCM aSource

Internal workhorse, expects value of --experimental-irrelevance flag as argument.

applyRelevanceToContext :: Relevance -> TCM a -> TCM aSource

(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

wakeIrrelevantVars :: TCM a -> TCM aSource

Wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.

Tests