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

Constructors

NoWithFunction

WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [NamedArg Pattern] Permutation Permutation Permutation [Clause]

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