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

Agda.TypeChecking.Rules.Term

Contents

Synopsis

Types

isType :: Expr -> Sort -> TCM TypeSource

Check that an expression is a type.

isType_ :: Expr -> TCM TypeSource

Check that an expression is a type without knowing the sort.

forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)Source

Force a type to be a Pi. Instantiates if necessary. The Hiding is only used when instantiating a meta variable.

Telescopes

checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM aSource

Type check a telescope. Binds the variables defined by the telescope.

checkTypedBindings :: TypedBindings -> (Telescope -> TCM a) -> TCM aSource

Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.

Literal

Terms

checkExpr :: Expr -> Type -> TCM TermSource

Type check an expression.

inferHead :: Head -> TCM (Args -> Term, Type)Source

Infer the type of a head thing (variable, function symbol, or constructor)

checkHeadApplication :: Expr -> Type -> Head -> [NamedArg Expr] -> TCM TermSource

checkHeadApplication e t hd args checks that e has type t, assuming that e has the form hd args. The corresponding type-checked term is returned.

If the head term hd is a coinductive constructor, then a top-level definition fresh tel = hd args (where the clause is delayed) is added, where tel corresponds to the current telescope. The returned term is fresh tel.

Precondition: The head hd has to be unambiguous, and there should not be any need to insert hidden lambdas.

traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM rSource

checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type, Constraints)Source

Check a list of arguments: checkArgs args t0 t1 checks that t0 = Delta -> t0' and args : Delta. Inserts hidden arguments to make this happen. Returns t0' and any constraints that have to be solve for everything to be well-formed. TODO: doesn't do proper blocking of terms

checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Constraints)Source

Check that a list of arguments fits a telescope.

inferExpr :: Expr -> TCM (Term, Type)Source

Infer the type of an expression. Implemented by checking agains a meta variable.

Let bindings