- traceFun :: String -> TCM a -> TCM a
- traceFun' :: Show a => String -> TCM a -> TCM a
- class Instantiate t where
- instantiate :: t -> TCM t
- class Reduce t where
- unfoldDefinition :: Bool -> (Term -> TCM (Blocked Term)) -> Term -> QName -> Args -> TCM (Blocked Term)
- class Normalise t where
- class InstantiateFull t where
- instantiateFull :: t -> TCM t
- telViewM :: 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 :: t -> TCM tSource
Instantiate Telescope | |
Instantiate LevelAtom | |
Instantiate PlusLevel | |
Instantiate Level | |
Instantiate Sort | |
Instantiate Elim | |
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 LevelAtom | |
Reduce PlusLevel | |
Reduce Level | |
Reduce Sort | |
Reduce Elim | |
Reduce Type | |
Reduce Term | |
Reduce Constraint | |
Reduce t => Reduce [t] | |
Reduce t => Reduce (Arg t) | |
(Raise 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 :: 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 LevelAtom | |
Normalise PlusLevel | |
Normalise Level | |
Normalise Sort | |
Normalise Elim | |
Normalise Type | |
Normalise Term | |
Normalise DisplayForm | |
Normalise Constraint | |
Normalise ProblemConstraint | |
Normalise t => Normalise [t] | |
Normalise a => Normalise (Maybe a) | |
Normalise t => Normalise (Arg t) | |
(Raise t, Normalise t) => Normalise (Abs t) | |
(Raise a, 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 :: t -> TCM tSource