Agda.TypeChecking.Irrelevance
Description
Irrelevant function types.
- unusableRelevance :: Relevance -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- ignoreForced :: Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- hideAndRelParams :: Arg a -> Arg a
- modifyArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a
- inverseApplyRelevance :: Relevance -> Arg a -> Arg a
- applyRelevance :: Relevance -> Arg a -> Arg a
- workOnTypes :: TCM a -> TCM a
- doWorkOnTypes :: TCM a -> TCM a
- workOnTypes' :: Bool -> TCM a -> TCM a
- applyRelevanceToContext :: Relevance -> TCM a -> TCM a
- wakeIrrelevantVars :: TCM a -> TCM a
Documentation
unusableRelevance :: Relevance -> Bool
data Relevance
see Agda.Syntax.Common
unusableRelevance rel == True
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeRelevance r x
returns the most irrelevant y
such that forall x
, y
we have
x
iff
moreRelevant
(r composeRelevance
y)(r
(Galois connection).
inverseComposeRelevance
x) moreRelevant
y
ignoreForced :: Relevance -> Relevance
For comparing Relevance
ignoring Forced
.
irrToNonStrict :: Relevance -> Relevance
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToIrr :: Relevance -> Relevance
Operations on Arg
.
hideAndRelParams :: Arg a -> Arg a
Prepare parts of a parameter telescope for abstraction in constructors and projections.
modifyArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a
modifyArgRelevance f arg
applies f
to the argRelevance
component of arg
.
inverseApplyRelevance :: Relevance -> Arg a -> Arg a
Used to modify context when going into a rel
argument.
applyRelevance :: Relevance -> Arg a -> Arg 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).
doWorkOnTypes :: TCM a -> TCM a
Call me if --experimental-irrelevance is set.
workOnTypes' :: Bool -> TCM a -> TCM a
Internal workhorse, expects value of --experimental-irrelevance flag as argument.
applyRelevanceToContext :: 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. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.