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

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

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

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

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

data WithFunctionProblem

Constructors

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

checkClause :: Type -> Clause -> TCM Clauses

Type check a function clause.

checkWithFunction :: WithFunctionProblem -> TCM ()

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

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

containsAbsurdPattern :: Pattern -> Bool

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

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