Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
PrecomputeFreeVars PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
PrecomputeFreeVars Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
PrecomputeFreeVars Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source #
PrecomputeFreeVars Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type 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 (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 (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' 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 (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Maybe a -> FV (Maybe a) Source #
PrecomputeFreeVars a => PrecomputeFreeVars [a] Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: [a] -> FV [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 -> VarSet Source #

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