Agda.TypeChecking.Irrelevance

Irrelevant function types.

Operations on Dom.

hideAndRelParams :: Dom a -> Dom a

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

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

Used to modify context when going into a rel argument.

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

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

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

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

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

applyRelevanceToContext :: MonadTCM tcm => Relevance -> tcm a -> tcm a

(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

Wake up irrelevant variables and make them relevant. This is used when type checking terms in a hole, in which case you want to be able to (for instance) infer the type of an irrelevant variable. In the course of type checking an irrelevant function argument applyRelevanceToContext is used instead, which also sets the context relevance to Irrelevant. This is not the right thing to do when type checking interactively in a hole since it also marks all metas created during type checking as irrelevant (issue #2568).

class UsableRelevance a where

Check whether something can be used in a position of the given relevance.

Minimal complete definition

usableRel

Methods

usableRel :: Relevance -> a -> TCM Bool

Instances

UsableRelevance LevelAtom

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> LevelAtom -> TCM Bool

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> PlusLevel -> TCM Bool

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Level -> TCM Bool

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Sort -> TCM Bool

UsableRelevance Term

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Term -> TCM Bool

UsableRelevance a => UsableRelevance [a]

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> [a] -> TCM Bool

UsableRelevance a => UsableRelevance (Dom a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Dom a -> TCM Bool

UsableRelevance a => UsableRelevance (Arg a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Arg a -> TCM Bool

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Type' a -> TCM Bool

(Subst t a, UsableRelevance a) => UsableRelevance (Abs a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Abs a -> TCM Bool

UsableRelevance a => UsableRelevance (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Elim' a -> TCM Bool

(UsableRelevance a, UsableRelevance b) => UsableRelevance (a, b)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> (a, b) -> TCM Bool