Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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 #


:: 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.

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.




mkBody :: Permutation -> Term -> ClauseBody Source #

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.

checkClause Source #


:: Type

Type of function defined by this clause.

-> SpineClause


-> TCM Clause

Type-checked clause.

Type check a function clause.

checkRHS Source #


:: 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.

checkWithRHS Source #


:: QName

Name of function.

-> QName

Name of the with-function.

-> Type

Type of function.

-> LHSResult

Result of type-checking patterns

-> [Term]


-> [EqualityView]

Types of with-expressions.

-> [Clause]

With-clauses to check.

-> TCM (ClauseBody, WithFunctionProblem) 

checkWhere Source #


:: Type

Type of rhs.

-> [Declaration]

Where-declarations to check.

-> TCM a


-> TCM a 

Type check a where clause.

containsAbsurdPattern :: Pattern -> Bool Source #

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