Safe Haskell | Safe-Infered |
---|
Agda.TypeChecking.Rules.Def
Contents
- checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- insertPatterns :: [Pattern] -> RHS -> RHS
- data WithFunctionProblem
- checkClause :: Type -> Clause -> TCM Clause
- checkWithFunction :: WithFunctionProblem -> TCM ()
- checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a
- containsAbsurdPattern :: Pattern -> Bool
- actualConstructor :: QName -> TCM QName
Definitions by pattern matching
checkFunDef' :: Type -> Relevance -> 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 Permutation [Clause] |
checkClause :: Type -> Clause -> TCM Clause
Type check a function clause.
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 :: QName -> TCM QName