Agda.TypeChecking.Rules.Def

Definitions by pattern matching

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()

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

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

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

Check a trivial definition of the form f = e

checkFunDef'

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 (Int, Int)

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.

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

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

data WithFunctionProblem

Parameters for creating a with-function.

Constructors

NoWithFunction

WithFunction

Fields

wfParentName :: QName

parent function name

wfName :: QName

with function name

wfParentTel :: Telescope

arguments to parent function

wfBeforeTel :: Telescope

arguments to the with function before the with expressions

wfAfterTel :: Telescope

arguments to the with function after the with expressions

wfExprs :: [Term]

with expressions

wfExprTypes :: [Type]

types of the with expressions

wfRHSType :: Type

type of the right hand side

wfParentPats :: [NamedArg Pattern]

parent patterns

wfPermSplit :: Permutation

permutation resulting from splitting the telescope into needed and unneeded vars

wfPermParent :: Permutation

permutation reordering the variables in the parent pattern

wfPermFinal :: Permutation

final permutation (including permutation for the parent clause)

wfClauses :: [Clause]

the given clauses for the with function

checkClause :: Type -> SpineClause -> TCM Clause

Type check a function clause.

checkWithFunction :: WithFunctionProblem -> TCM ()

checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a

Type check a where clause. The first argument is the number of variables bound in the left hand side.

containsAbsurdPattern :: Pattern -> Bool

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