Agda-2.2.10: A dependently typed functional programming language and proof assistant

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)

TODO: move to Agda.Syntax.Abstract.View

expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)

TODO: move somewhere else

splitProblem :: Problem -> TCM (Either SplitError SplitProblem)

Split a problem at the first constructor of datatype type. Implicit patterns should have been inserted.

wellFormedIndices

Arguments

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