- 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