Safe Haskell | Safe-Infered |
---|
- 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 ()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
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 ()
actualConstructor :: QName -> TCM QNameSource