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

Agda.TypeChecking.Rules.Def

Contents

Synopsis

# Definitions by pattern matching

isAlias :: [Clause] -> Type -> Maybe (Expr, MetaId) Source #

A single clause without arguments and without type signature is an alias.

checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> TCM () Source #

Check a trivial definition of the form f = e

Arguments

 :: Type the type we expect the function to have -> ArgInfo is it irrelevant (for instance) -> Delayed are the clauses delayed (not unfolded willy-nilly) -> Maybe ExtLamInfo does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args) -> Maybe QName is it a with function (if so, what's the name of the parent function) -> DefInfo range info -> QName the name of the function -> [Clause] the clauses to check -> TCM ()

Type check a definition by pattern matching.

Set funTerminates according to termination info in TCEnv, which comes from a possible termination pragma.

insertPatterns :: [Pattern] -> RHS -> RHS Source #

Insert some patterns in the in with-clauses LHS of the given RHS

Parameters for creating a with-function.

Constructors

 NoWithFunction WithFunction FieldswfParentName :: QNameParent function name.wfName :: QNameWith function name.wfParentType :: TypeType of the parent function.wfBeforeTel :: TelescopeTypes of arguments to the with function before the with expressions (needed vars).wfAfterTel :: TelescopeTypes of arguments to the with function after the with expressions (unneeded vars).wfExprs :: [Term]With and rewrite expressions.wfExprTypes :: [EqualityView]Types of the with and rewrite expressions.wfRHSType :: TypeType of the right hand side.wfParentPats :: [NamedArg Pattern]Parent patterns.wfPermSplit :: PermutationPermutation resulting from splitting the telescope into needed and unneeded vars.wfPermParent :: PermutationPermutation reordering the variables in the parent pattern.wfPermFinal :: PermutationFinal permutation (including permutation for the parent clause).wfClauses :: [Clause]The given clauses for the with function

Create a clause body from a term.

As we have type checked the term in the clause telescope, but the final body should have bindings in the order of the pattern variables, we need to apply the permutation to the checked term.

Arguments

 :: Type Type of function defined by this clause. -> SpineClause Clause. -> TCM Clause Type-checked clause.

Type check a function clause.

Arguments

 :: LHSInfo Range of lhs. -> QName Name of function. -> [NamedArg Pattern] Patterns in lhs. -> Type Type of function. -> LHSResult Result of type-checking patterns -> RHS Rhs to check. -> TCM (ClauseBody, WithFunctionProblem)

Type check the with and rewrite lhss and/or the rhs.

Arguments

 :: QName Name of function. -> QName Name of the with-function. -> Type Type of function. -> LHSResult Result of type-checking patterns -> [Term] With-expressions. -> [EqualityView] Types of with-expressions. -> [Clause] With-clauses to check. -> TCM (ClauseBody, WithFunctionProblem)

Arguments

 :: Type Type of rhs. -> [Declaration] Where-declarations to check. -> TCM a Continuation. -> TCM a

Type check a where clause.

Check if a pattern contains an absurd pattern. For instance, suc ()