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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Irrelevance

Contents

Description

Irrelevant function types.

Synopsis

Operations on Dom.

hideAndRelParams :: Dom a -> Dom a Source

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

inverseApplyRelevance :: Relevance -> Dom a -> Dom a Source

Used to modify context when going into a rel argument.

applyRelevance :: Relevance -> Dom a -> Dom a Source

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 a Source

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 a Source

Call me if --experimental-irrelevance is set.

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

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

applyRelevanceToContext :: Relevance -> TCM a -> TCM a Source

(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 a Source

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