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

Safe HaskellNone
LanguageHaskell98

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

checkFunDef' Source

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.

useTerPragma :: Definition -> TCM Definition Source

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

data WithFunctionProblem Source

Parameters for creating a with-function.

Constructors

NoWithFunction 
WithFunction 

Fields

wfParentName :: QName

Parent function name.

wfName :: QName

With function name.

wfParentType :: Type

Type of the parent function.

wfBeforeTel :: Telescope

Types of arguments to the with function before the with expressions (needed vars).

wfAfterTel :: Telescope

Types of arguments to the with function after the with expressions (unneeded vars).

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 Source

Type check a function clause.

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

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

containsAbsurdPattern :: Pattern -> Bool Source

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