Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Rules.LHS.Split
Synopsis
asView :: Pattern -> ([Name], Pattern)
expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)
splitProblem :: Problem -> TCM (Either SplitError SplitProblem)
wellFormedIndices :: MonadTCM tcm => [Arg Term] -> [Arg Term] -> tcm ()
Documentation
asView :: Pattern -> ([Name], Pattern)Source
TODO: move to Agda.Syntax.Abstract.View
expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)Source
TODO: move somewhere else
splitProblem :: Problem -> TCM (Either SplitError SplitProblem)Source
Split a problem at the first constructor of datatype type. Implicit patterns should have been inserted.
wellFormedIndicesSource
:: MonadTCM tcm
=> [Arg Term]Parameters.
-> [Arg Term]Indices.
-> tcm ()
Checks that the indices are constructors applied to distinct variables which do not occur free in the parameters.
Produced by Haddock version 2.6.1