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

Agda.TypeChecking.Reduce

Contents

Normalisation
Full instantiation

Synopsis

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

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

traceFun :: MonadTCM tcm => String -> tcm a -> tcm a | Source

traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a | Source

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 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)

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 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

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