Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Reduce

Contents Normalisation Full instantiation

Synopsis

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 reduce :: MonadTCM tcm => t -> tcm t reduceB :: MonadTCM tcm => t -> tcm (Blocked t) unfoldDefinition :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term) class Normalise t where normalise :: MonadTCM tcm => t -> tcm t class InstantiateFull t where instantiateFull :: MonadTCM tcm => t -> tcm t telViewM :: MonadTCM tcm => Type -> tcm TelView

Documentation

traceFun :: MonadTCM tcm => String -> tcm a -> tcm a Source

traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a Source

class Instantiate t where Source

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 t Source

class Reduce t where Source

Methods reduce :: MonadTCM tcm => t -> tcm t Source reduceB :: MonadTCM tcm => t -> tcm (Blocked t) Source

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

class Normalise t where Source

Methods normalise :: MonadTCM tcm => t -> tcm t Source

Full instantiation

class InstantiateFull t where Source

Methods instantiateFull :: MonadTCM tcm => t -> tcm t Source

telViewM :: MonadTCM tcm => Type -> tcm TelView Source

Produced by Haddock version 2.6.0