- 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).
instantiate :: MonadTCM tcm => t -> tcm tSource
Instantiate Telescope | |
Instantiate Sort | |
Instantiate Type | |
Instantiate Term | |
Instantiate Constraint | |
Instantiate t => Instantiate [t] | |
Instantiate t => Instantiate (Arg t) | |
Instantiate t => Instantiate (Abs t) | |
Instantiate a => Instantiate (Blocked a) | |
Instantiate a => Instantiate (Closure a) | |
(Instantiate a, Instantiate b) => Instantiate (a, b) | |
(Ord k, Instantiate e) => Instantiate (Map k e) | |
(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) |
Reduce Telescope | |
Reduce Sort | |
Reduce Type | |
Reduce Term | |
Reduce Constraint | |
Reduce t => Reduce [t] | |
Reduce t => Reduce (Arg t) | |
Reduce t => Reduce (Abs t) | |
Reduce a => Reduce (Closure a) | |
(Reduce a, Reduce b) => Reduce (a, b) | |
(Ord k, Reduce e) => Reduce (Map k e) | |
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) |
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
Normalise Pattern | |
Normalise ClauseBody | |
Normalise Sort | |
Normalise Type | |
Normalise Term | |
Normalise DisplayForm | |
Normalise Constraint | |
Normalise t => Normalise [t] | |
Normalise a => Normalise (Maybe a) | |
Normalise t => Normalise (Arg t) | |
Normalise t => Normalise (Abs t) | |
Normalise a => Normalise (Tele a) | |
Normalise a => Normalise (Closure a) | |
(Normalise a, Normalise b) => Normalise (a, b) | |
(Ord k, Normalise e) => Normalise (Map k e) | |
(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) |
Full instantiation
class InstantiateFull t whereSource
instantiateFull :: MonadTCM tcm => t -> tcm tSource