Safe Haskell | Safe-Infered |
---|
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
inverseComposeRelevance :: Relevance -> Relevance -> RelevanceSource
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 -> RelevanceSource
For comparing Relevance
ignoring Forced
.
irrToNonStrict :: Relevance -> RelevanceSource
Irrelevant function arguments may appear non-strictly in the codomain type.
Operations on Arg
.
hideAndRelParams :: Arg a -> Arg aSource
Prepare parts of a parameter telescope for abstraction in constructors and projections.
modifyArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg aSource
modifyArgRelevance f arg
applies f
to the argRelevance
component of arg
.
inverseApplyRelevance :: Relevance -> Arg a -> Arg aSource
Used to modify context when going into a rel
argument.
applyRelevance :: Relevance -> Arg a -> Arg 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.