Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

PrecomputeFreeVars PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

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

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 #