Safe Haskell | None |
---|
- asView :: Pattern -> ([Name], Pattern)
- expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)
- splitProblem :: Problem -> TCM (Either SplitError SplitProblem)
- wellFormedIndices :: Type -> TCM ()
- withTypesFrom :: Args -> Type -> TCM [(Arg Term, Dom Type)]
Documentation
splitProblem :: Problem -> TCM (Either SplitError SplitProblem)Source
Split a problem at the first constructor of datatype type. Implicit patterns should have been inserted.
wellFormedIndices :: Type -> TCM ()Source
Takes a type, which must be a data or record type application, and checks that the indices are constructors (or literals) applied to distinct variables which do not occur free in the parameters. For the purposes of this check parameters count as constructor arguments; parameters are reconstructed from the given type.
Precondition: The type must be a data or record type application.