Safe Haskell | None |
---|---|
Language | Haskell2010 |
Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
Synopsis
- class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a
- forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a)
- data IsFree
Documentation
class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a Source #
forceNotFree'
Instances
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a) Source #
Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and for each of the given variables whether it is either not free, or maybe free depending on some metavariables.