Agda.TypeChecking.Free.Reduce

Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.

Documentation

class (PrecomputeFreeVars a, Subst a) => ForceNotFree a

Minimal complete definition

forceNotFree'

Instances

ForceNotFree PlusLevel

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel

ForceNotFree Level

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Level -> m Level

ForceNotFree Sort

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Sort -> m Sort

ForceNotFree Type

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Type -> m Type

ForceNotFree Term

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Term -> m Term

ForceNotFree a => ForceNotFree [a]

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => [a] -> m [a]

(Reduce a, ForceNotFree a) => ForceNotFree (Arg a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a)

(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)

(Reduce a, ForceNotFree a) => ForceNotFree (Abs a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a)

(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a)

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)

forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a)

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.

data IsFree

A variable can either not occur (NotFree) or it does occur (MaybeFree). In the latter case, the occurrence may disappear depending on the instantiation of some set of metas.

Constructors

MaybeFree MetaSet

NotFree

Instances

Eq IsFree

Defined in Agda.TypeChecking.Free.Reduce

Methods

(==) :: IsFree -> IsFree -> Bool

(/=) :: IsFree -> IsFree -> Bool

Show IsFree

Defined in Agda.TypeChecking.Free.Reduce

Methods

showsPrec :: Int -> IsFree -> ShowS

show :: IsFree -> String

showList :: [IsFree] -> ShowS