Agda.TypeChecking.Reduce
Contents
- traceFun :: MonadTCM tcm => String -> tcm a -> tcm a
- traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a
- class Instantiate t where
- instantiate :: MonadTCM tcm => t -> tcm t
- class Reduce t where
- unfoldDefinition :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term)
- class Normalise t where
- class InstantiateFull t where
- instantiateFull :: MonadTCM tcm => t -> tcm t
- telViewM :: MonadTCM tcm => Type -> tcm TelView
Documentation
class Instantiate t whereSource
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).
Methods
instantiate :: MonadTCM tcm => t -> tcm tSource
unfoldDefinition :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term)Source
If the first argument is True, then a single delayed clause may
be unfolded.
Normalisation
Full instantiation
class InstantiateFull t whereSource
Methods
instantiateFull :: MonadTCM tcm => t -> tcm tSource