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




Definitions by pattern matching

checkFunDef :: 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 ClausesSource

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