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

Safe HaskellNone

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

Reduction to weak head normal form.

ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a

ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a

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.

reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)

Reduce a non-primitive definition if it is a copy linking to another def.

reduceDef :: QName -> Args -> TCM (Reduced () Term)

Reduce a non-primitive definition once unless it is delayed.

Normalisation

Full instantiation

class InstantiateFull t where

Methods

instantiateFull :: t -> TCM t

Instances

InstantiateFull Char 
InstantiateFull ModuleName 
InstantiateFull QName 
InstantiateFull Name 
InstantiateFull Scope 
InstantiateFull Pattern 
InstantiateFull ClauseBody 
InstantiateFull Clause 
InstantiateFull LevelAtom 
InstantiateFull PlusLevel 
InstantiateFull Level 
InstantiateFull Sort 
InstantiateFull Type 
InstantiateFull Elim 
InstantiateFull Term 
InstantiateFull CompiledClauses 
InstantiateFull FunctionInverse 
InstantiateFull Defn 
InstantiateFull Definition 
InstantiateFull DisplayTerm 
InstantiateFull DisplayForm 
InstantiateFull Section 
InstantiateFull Signature 
InstantiateFull Constraint 
InstantiateFull ProblemConstraint 
InstantiateFull Interface 
InstantiateFull t => InstantiateFull [t] 
InstantiateFull a => InstantiateFull (Maybe a) 
InstantiateFull t => InstantiateFull (Arg t) 
InstantiateFull t => InstantiateFull (Dom t) 
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) 
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) 
InstantiateFull a => InstantiateFull (Case a) 
InstantiateFull a => InstantiateFull (WithArity a) 
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) 
(Eq k, Hashable k, InstantiateFull e) => InstantiateFull (HashMap k e) 
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c)