Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 -> RHSSource
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 ClauseSource
Type check a function clause.
checkWithFunction :: WithFunctionProblem -> TCM ()Source
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 :: MonadTCM tcm => QName -> tcm QNameSource
Produced by Haddock version 2.6.0