Agda.TypeChecking.Free.Precompute

Precompute free variables in a term (and store in ArgInfo).

Documentation

class PrecomputeFreeVars a where

Methods

precomputeFreeVars :: a -> FV a

precomputeFreeVars :: (Traversable c, PrecomputeFreeVars x, a ~ c x) => a -> FV a

Instances

PrecomputeFreeVars LevelAtom

Methods

precomputeFreeVars :: LevelAtom -> FV LevelAtom

PrecomputeFreeVars PlusLevel

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel

PrecomputeFreeVars Level

Methods

precomputeFreeVars :: Level -> FV Level

PrecomputeFreeVars Sort

Methods

precomputeFreeVars :: Sort -> FV Sort

PrecomputeFreeVars Type

Methods

precomputeFreeVars :: Type -> FV Type

PrecomputeFreeVars Term

Methods

precomputeFreeVars :: Term -> FV Term

PrecomputeFreeVars a => PrecomputeFreeVars [a]

Methods

precomputeFreeVars :: [a] -> FV [a]

PrecomputeFreeVars a => PrecomputeFreeVars (Maybe a)

Methods

precomputeFreeVars :: Maybe a -> FV (Maybe a)

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Methods

precomputeFreeVars :: Dom a -> FV (Dom a)

PrecomputeFreeVars a => PrecomputeFreeVars (Arg a)

Methods

precomputeFreeVars :: Arg a -> FV (Arg a)

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a)

Methods

precomputeFreeVars :: Abs a -> FV (Abs a)

PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)

Methods

precomputeFreeVars :: Elim' a -> FV (Elim' a)

(PrecomputeFreeVars a, PrecomputeFreeVars b) => PrecomputeFreeVars (a, b)

Methods

precomputeFreeVars :: (a, b) -> FV (a, b)

precomputeFreeVars :: PrecomputeFreeVars a => a -> FV a

precomputedFreeVars :: PrecomputeFreeVars a => a -> IntSet

precomputeFreeVars_ :: PrecomputeFreeVars a => a -> a