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.6.0