Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Free.Precompute

Description

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

Documentation

class PrecomputeFreeVars a Source #

Instances

Instances details

PrecomputeFreeVars PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
PrecomputeFreeVars Level Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
PrecomputeFreeVars Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
PrecomputeFreeVars Type Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
PrecomputeFreeVars Term Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source #
PrecomputeFreeVars a => PrecomputeFreeVars [a] Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: [a] -> FV [a] Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Maybe a -> FV (Maybe a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Arg a -> FV (Arg a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source #
(PrecomputeFreeVars a, PrecomputeFreeVars b) => PrecomputeFreeVars (a, b) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: (a, b) -> FV (a, b) Source #

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

precomputedFreeVars :: PrecomputeFreeVars a => a -> IntSet Source #

precomputeFreeVars_ :: PrecomputeFreeVars a => a -> a Source #