Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered

Agda.TypeChecking.Reduce

Contents

Synopsis

Documentation

traceFun :: String -> TCM a -> TCM a

traceFun' :: Show a => String -> TCM a -> TCM a

class Instantiate t where

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 :: t -> TCM t

class Reduce t where

Methods

reduce :: t -> TCM t

reduceB :: t -> TCM (Blocked t)

Instances

unfoldDefinition :: Bool -> (Term -> TCM (Blocked Term)) -> Term -> QName -> Args -> TCM (Blocked Term)

If the first argument is True, then a single delayed clause may be unfolded.

Normalisation

Full instantiation

telViewM :: Type -> TCM TelView

telViewM t is like telView' t, but it reduces t to expose function type constructors.