Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Free.Precompute

Description

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

Documentation

class PrecomputeFreeVars a #

Instances

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

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

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

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