Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 aSource
traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm aSource
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
class Reduce t whereSource
Methods
reduce :: MonadTCM tcm => t -> tcm tSource
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 whereSource
Methods
normalise :: MonadTCM tcm => t -> tcm tSource
Full instantiation
class InstantiateFull t whereSource
Methods
instantiateFull :: MonadTCM tcm => t -> tcm tSource
telViewM :: MonadTCM tcm => Type -> tcm TelViewSource
Produced by Haddock version 2.6.0