- 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