| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.LHS.Split

Synopsis

asView :: Pattern -> ([Name], Pattern)
expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)
splitProblem :: Problem -> TCM (Either SplitError SplitProblem)

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.
Produced by Haddock version 2.4.2