Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Reduce

Contents

Reduction to weak head normal form.
Simplification
Normalisation
Full instantiation

Synopsis

instantiate :: Instantiate a => a -> TCM a
instantiateFull :: InstantiateFull a => a -> TCM a
reduce :: Reduce a => a -> TCM a
reduceB :: Reduce a => a -> TCM (Blocked a)
normalise :: Normalise a => a -> TCM a
simplify :: Simplify a => a -> TCM a
isFullyInstantiatedMeta :: MetaId -> TCM Bool
class Instantiate t where
ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (NotBlocked -> Term -> tcm a) -> tcm a
isBlocked :: MonadTCM tcm => Term -> tcm (Maybe MetaId)
ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (NotBlocked -> Type -> tcm a) -> tcm a
isBlockedType :: MonadTCM tcm => Type -> tcm (Maybe MetaId)
class Reduce t where
shouldTryFastReduce :: ReduceM Bool
maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm :: Term -> ReduceM (Blocked Term)
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursion :: Term -> ReduceM (Blocked Term)
unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term)
unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinition' :: Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term)
reduceHead :: Term -> TCM (Blocked Term)
reduceHead' :: Term -> ReduceM (Blocked Term)
unfoldInlined :: Term -> TCM Term
unfoldInlined' :: Term -> ReduceM Term
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
class Simplify t where
simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
class Normalise t where
slowNormaliseArgs :: Term -> ReduceM Term
class InstantiateFull t where

Documentation

instantiate :: Instantiate a => a -> TCM a #

instantiateFull :: InstantiateFull a => a -> TCM a #

reduce :: Reduce a => a -> TCM a #

reduceB :: Reduce a => a -> TCM (Blocked a) #

normalise :: Normalise a => a -> TCM a #

simplify :: Simplify a => a -> TCM a #

isFullyInstantiatedMeta :: MetaId -> TCM Bool #

Meaning no metas left in the instantiation.

class Instantiate t where #

Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).

Minimal complete definition

instantiate'

Methods

instantiate' :: t -> ReduceM t #

Instances

Instantiate EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView #
Instantiate LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: LevelAtom -> ReduceM LevelAtom #
Instantiate PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel -> ReduceM PlusLevel #
Instantiate Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level #
Instantiate Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort #
Instantiate Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope #
Instantiate Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type -> ReduceM Type #
Instantiate Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim -> ReduceM Elim #
Instantiate Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Term -> ReduceM Term #
Instantiate Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Candidate -> ReduceM Candidate #
Instantiate Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Constraint -> ReduceM Constraint #
Instantiate t => Instantiate [t] #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: [t] -> ReduceM [t] #
Instantiate t => Instantiate (Dom t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Dom t -> ReduceM (Dom t) #
Instantiate t => Instantiate (Arg t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Arg t -> ReduceM (Arg t) #
Instantiate a => Instantiate (Blocked a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) #
Instantiate t => Instantiate (Abs t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) #
Instantiate a => Instantiate (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Closure a -> ReduceM (Closure a) #
(Instantiate a, Instantiate b) => Instantiate (a, b) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: (a, b) -> ReduceM (a, b) #
Instantiate e => Instantiate (Map k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Map k e -> ReduceM (Map k e) #
(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: (a, b, c) -> ReduceM (a, b, c) #

Reduction to weak head normal form.

ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (NotBlocked -> Term -> tcm a) -> tcm a #

Case on whether a term is blocked on a meta (or is a meta). That means it can change its shape when the meta is instantiated.

isBlocked :: MonadTCM tcm => Term -> tcm (Maybe MetaId) #

ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (NotBlocked -> Type -> tcm a) -> tcm a #

Case on whether a type is blocked on a meta (or is a meta).

isBlockedType :: MonadTCM tcm => Type -> tcm (Maybe MetaId) #

class Reduce t where #

Methods

reduce' :: t -> ReduceM t #

reduceB' :: t -> ReduceM (Blocked t) #

Instances

Reduce EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) #
Reduce LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: LevelAtom -> ReduceM LevelAtom # reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom) #
Reduce PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) #
Reduce Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level # reduceB' :: Level -> ReduceM (Blocked Level) #
Reduce Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort # reduceB' :: Sort -> ReduceM (Blocked Sort) #
Reduce Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope # reduceB' :: Telescope -> ReduceM (Blocked Telescope) #
Reduce Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type # reduceB' :: Type -> ReduceM (Blocked Type) #
Reduce Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim # reduceB' :: Elim -> ReduceM (Blocked Elim) #
Reduce Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term # reduceB' :: Term -> ReduceM (Blocked Term) #
Reduce Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Candidate -> ReduceM Candidate # reduceB' :: Candidate -> ReduceM (Blocked Candidate) #
Reduce Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Constraint -> ReduceM Constraint # reduceB' :: Constraint -> ReduceM (Blocked Constraint) #
Reduce t => Reduce [t] #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: [t] -> ReduceM [t] # reduceB' :: [t] -> ReduceM (Blocked [t]) #
Reduce t => Reduce (Dom t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Dom t -> ReduceM (Dom t) # reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) #
Reduce t => Reduce (Arg t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Arg t -> ReduceM (Arg t) # reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) #
(Subst t a, Reduce a) => Reduce (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Abs a -> ReduceM (Abs a) # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) #
Reduce a => Reduce (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Closure a -> ReduceM (Closure a) # reduceB' :: Closure a -> ReduceM (Blocked (Closure a)) #
(Reduce a, Reduce b) => Reduce (a, b) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: (a, b) -> ReduceM (a, b) # reduceB' :: (a, b) -> ReduceM (Blocked (a, b)) #
Reduce e => Reduce (Map k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Map k e -> ReduceM (Map k e) # reduceB' :: Map k e -> ReduceM (Blocked (Map k e)) #
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: (a, b, c) -> ReduceM (a, b, c) # reduceB' :: (a, b, c) -> ReduceM (Blocked (a, b, c)) #

shouldTryFastReduce :: ReduceM Bool #

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term) #

slowReduceTerm :: Term -> ReduceM (Blocked Term) #

unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim) #

unfoldCorecursion :: Term -> ReduceM (Blocked Term) #

unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term) #

If the first argument is True, then a single delayed clause may be unfolded.

unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term) #

unfoldDefinition' :: Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) #

unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term) #

reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term) #

Reduce a non-primitive definition if it is a copy linking to another def.

reduceHead :: Term -> TCM (Blocked Term) #

Reduce simple (single clause) definitions.

reduceHead' :: Term -> ReduceM (Blocked Term) #

unfoldInlined :: Term -> TCM Term #

Unfold a single inlined function.

unfoldInlined' :: Term -> ReduceM Term #

appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) #

Apply a definition using the compiled clauses, or fall back to ordinary clauses if no compiled clauses exist.

appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) #

appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) #

Apply a defined function to it's arguments, using the compiled clauses. The original term is the first argument applied to the third.

appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) #

appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) #

Apply a defined function to it's arguments, using the original clauses.

appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) #

Simplification

class Simplify t where #

Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched.

Minimal complete definition

simplify'

Methods

simplify' :: t -> ReduceM t #

Instances

Simplify Bool #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Bool -> ReduceM Bool #
Simplify EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: EqualityView -> ReduceM EqualityView #
Simplify LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: LevelAtom -> ReduceM LevelAtom #
Simplify PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel #
Simplify Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level #
Simplify Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort #
Simplify Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type -> ReduceM Type #
Simplify Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim -> ReduceM Elim #
Simplify Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term #
Simplify Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Candidate -> ReduceM Candidate #
Simplify DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: DisplayForm -> ReduceM DisplayForm #
Simplify Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Constraint -> ReduceM Constraint #
Simplify ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: ProblemConstraint -> ReduceM ProblemConstraint #
Simplify t => Simplify [t] #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: [t] -> ReduceM [t] #
Simplify a => Simplify (Maybe a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Maybe a -> ReduceM (Maybe a) #
Simplify t => Simplify (Dom t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t) #
Simplify t => Simplify (Arg t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Arg t -> ReduceM (Arg t) #
(Subst t a, Simplify a) => Simplify (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Tele a -> ReduceM (Tele a) #
(Subst t a, Simplify a) => Simplify (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a) #
Simplify a => Simplify (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Closure a -> ReduceM (Closure a) #
(Simplify a, Simplify b) => Simplify (a, b) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: (a, b) -> ReduceM (a, b) #
Simplify e => Simplify (Map k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Map k e -> ReduceM (Map k e) #
Simplify t => Simplify (Named name t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Named name t -> ReduceM (Named name t) #
(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: (a, b, c) -> ReduceM (a, b, c) #

simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t #

Normalisation

class Normalise t where #

Minimal complete definition

normalise'

Methods

normalise' :: t -> ReduceM t #

Instances

Normalise Bool #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Bool -> ReduceM Bool #
Normalise Char #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Char -> ReduceM Char #
Normalise Int #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Int -> ReduceM Int #
Normalise EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: EqualityView -> ReduceM EqualityView #
Normalise ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo #
Normalise DBPatVar #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DBPatVar -> ReduceM DBPatVar #
Normalise LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: LevelAtom -> ReduceM LevelAtom #
Normalise PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel #
Normalise Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level #
Normalise Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort #
Normalise Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type -> ReduceM Type #
Normalise Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim -> ReduceM Elim #
Normalise Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Term -> ReduceM Term #
Normalise Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Candidate -> ReduceM Candidate #
Normalise DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DisplayForm -> ReduceM DisplayForm #
Normalise Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Constraint -> ReduceM Constraint #
Normalise ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ProblemConstraint -> ReduceM ProblemConstraint #
Normalise t => Normalise [t] #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: [t] -> ReduceM [t] #
Normalise a => Normalise (Maybe a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Maybe a -> ReduceM (Maybe a) #
Normalise t => Normalise (Dom t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) #
Normalise t => Normalise (Arg t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Arg t -> ReduceM (Arg t) #
Normalise a => Normalise (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Pattern' a -> ReduceM (Pattern' a) #
(Subst t a, Normalise a) => Normalise (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Tele a -> ReduceM (Tele a) #
(Subst t a, Normalise a) => Normalise (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) #
Normalise a => Normalise (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Closure a -> ReduceM (Closure a) #
(Normalise a, Normalise b) => Normalise (a, b) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: (a, b) -> ReduceM (a, b) #
Normalise e => Normalise (Map k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Map k e -> ReduceM (Map k e) #
Normalise t => Normalise (Named name t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Named name t -> ReduceM (Named name t) #
(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: (a, b, c) -> ReduceM (a, b, c) #

slowNormaliseArgs :: Term -> ReduceM Term #

Full instantiation

class InstantiateFull t where #

instantiateFull' instantiates metas everywhere (and recursively) but does not reduce.

Minimal complete definition

instantiateFull'

Methods

instantiateFull' :: t -> ReduceM t #

Instances

InstantiateFull Bool #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Bool -> ReduceM Bool #
InstantiateFull Char #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Char -> ReduceM Char #
InstantiateFull Int #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Int -> ReduceM Int #
InstantiateFull ModuleName #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName #
InstantiateFull QName #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: QName -> ReduceM QName #
InstantiateFull Name #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Name -> ReduceM Name #
InstantiateFull Scope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope #
InstantiateFull EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: EqualityView -> ReduceM EqualityView #
InstantiateFull Substitution #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution #
InstantiateFull ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo #
InstantiateFull DBPatVar #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DBPatVar -> ReduceM DBPatVar #
InstantiateFull Clause #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Clause -> ReduceM Clause #
InstantiateFull LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: LevelAtom -> ReduceM LevelAtom #
InstantiateFull PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel #
InstantiateFull Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level #
InstantiateFull Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort #
InstantiateFull Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Term -> ReduceM Term #
InstantiateFull ConHead #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead #
InstantiateFull CompiledClauses #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses #
InstantiateFull Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Candidate -> ReduceM Candidate #
InstantiateFull FunctionInverse #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse #
InstantiateFull Defn #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Defn -> ReduceM Defn #
InstantiateFull Definition #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Definition -> ReduceM Definition #
InstantiateFull RewriteRule #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: RewriteRule -> ReduceM RewriteRule #
InstantiateFull NLPType #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPType -> ReduceM NLPType #
InstantiateFull NLPat #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPat -> ReduceM NLPat #
InstantiateFull DisplayTerm #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm #
InstantiateFull DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayForm -> ReduceM DisplayForm #
InstantiateFull Section #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Section -> ReduceM Section #
InstantiateFull Signature #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Signature -> ReduceM Signature #
InstantiateFull Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Constraint -> ReduceM Constraint #
InstantiateFull ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint #
InstantiateFull Interface #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Interface -> ReduceM Interface #
InstantiateFull AsBinding #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods instantiateFull' :: AsBinding -> ReduceM AsBinding #
InstantiateFull LHSResult #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods instantiateFull' :: LHSResult -> ReduceM LHSResult #
InstantiateFull t => InstantiateFull [t] #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: [t] -> ReduceM [t] #
InstantiateFull a => InstantiateFull (Maybe a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Maybe a -> ReduceM (Maybe a) #
InstantiateFull t => InstantiateFull (Dom t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Dom t -> ReduceM (Dom t) #
InstantiateFull t => InstantiateFull (Arg t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Arg t -> ReduceM (Arg t) #
InstantiateFull a => InstantiateFull (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) #
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Tele a -> ReduceM (Tele a) #
InstantiateFull a => InstantiateFull (Type' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Type' a -> ReduceM (Type' a) #
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) #
InstantiateFull a => InstantiateFull (Elim' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' a -> ReduceM (Elim' a) #
InstantiateFull a => InstantiateFull (Case a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Case a -> ReduceM (Case a) #
InstantiateFull a => InstantiateFull (WithArity a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity a -> ReduceM (WithArity a) #
InstantiateFull a => InstantiateFull (Builtin a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Builtin a -> ReduceM (Builtin a) #
InstantiateFull a => InstantiateFull (Open a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Open a -> ReduceM (Open a) #
InstantiateFull a => InstantiateFull (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Closure a -> ReduceM (Closure a) #
(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: (a, b) -> ReduceM (a, b) #
InstantiateFull e => InstantiateFull (Map k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Map k e -> ReduceM (Map k e) #
InstantiateFull e => InstantiateFull (HashMap k e) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: HashMap k e -> ReduceM (HashMap k e) #
InstantiateFull t => InstantiateFull (Named name t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Named name t -> ReduceM (Named name t) #
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: (a, b, c) -> ReduceM (a, b, c) #