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

Agda.TypeChecking.Rules.Def

Contents

Synopsis

Definitions by pattern matching

checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()Source

Type check a definition by pattern matching. The first argument specifies whether the clauses are delayed or not.

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

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

checkClause :: Type -> Clause -> TCM ClauseSource

Type check a function clause.

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

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

containsAbsurdPattern :: Pattern -> BoolSource

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