Agda-2.2.4: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Reduce

Contents Normalisation Full instantiation

Synopsis

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

class Instantiate t where Source

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 t Source Instances Instantiate Telescope Instantiate Sort Instantiate Type Instantiate Term Instantiate Constraint Instantiate t => Instantiate ([] t) Instantiate t => Instantiate (Arg 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)

class Reduce t where Source

Methods reduce :: MonadTCM tcm => t -> tcm t Source reduceB :: MonadTCM tcm => t -> tcm (Blocked t) Source Instances Reduce Telescope Reduce Sort Reduce Type Reduce Term Reduce Constraint Reduce t => Reduce ([] t) Reduce t => Reduce (Arg 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

class Normalise t where Source

Methods normalise :: MonadTCM tcm => t -> tcm t Source Instances Normalise Pattern Normalise ClauseBody Normalise Telescope Normalise Sort Normalise Type Normalise Term Normalise DisplayForm Normalise Constraint Normalise t => Normalise ([] t) Normalise t => Normalise (Arg t) Normalise t => Normalise (Abs t) 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 where Source

Methods instantiateFull :: MonadTCM tcm => t -> tcm t Source Instances InstantiateFull Char InstantiateFull ModuleName InstantiateFull Name InstantiateFull ClauseBody InstantiateFull Clause InstantiateFull Telescope InstantiateFull Sort InstantiateFull Type InstantiateFull Term InstantiateFull Scope InstantiateFull FunctionInverse InstantiateFull Defn InstantiateFull Definition InstantiateFull DisplayTerm InstantiateFull DisplayForm InstantiateFull Section InstantiateFull Signature InstantiateFull Constraint InstantiateFull Interface InstantiateFull t => InstantiateFull ([] t) InstantiateFull a => InstantiateFull (Maybe a) InstantiateFull t => InstantiateFull (Arg t) InstantiateFull t => InstantiateFull (Abs t) InstantiateFull a => InstantiateFull (Builtin a) InstantiateFull a => InstantiateFull (Open a) InstantiateFull a => InstantiateFull (Closure a) (InstantiateFull a, InstantiateFull b) => InstantiateFull ((,) a b) (Ord k, InstantiateFull e) => InstantiateFull (Map k e) (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull ((,,) a b c)

telViewM :: MonadTCM tcm => Type -> tcm TelView Source

Produced by Haddock version 2.4.2