| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.Def

Contents

Definitions by pattern matching

Synopsis

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
insertPatterns :: [Pattern] -> RHS -> RHS

data WithFunctionProblem

= NoWithFunction
| WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [Arg Pattern] Permutation [Clause]

checkClause :: Type -> Clause -> TCM Clause
checkWithFunction :: WithFunctionProblem -> TCM ()
checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a
containsAbsurdPattern :: Pattern -> Bool
actualConstructor :: MonadTCM tcm => QName -> tcm QName

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 -> RHS | Source

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

data WithFunctionProblem | Source

Constructors

NoWithFunction |
WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [Arg Pattern] Permutation [Clause] |

checkClause :: Type -> Clause -> TCM Clause | Source

Type check a function clause.

checkWithFunction :: WithFunctionProblem -> TCM () | Source

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

actualConstructor :: MonadTCM tcm => QName -> tcm QName | Source

Produced by Haddock version 2.4.2