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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.LHS.Split

Synopsis

Documentation

splitProblem Source #

Arguments

:: Maybe QName

The definition we are checking at the moment.

-> Problem

The current state of the lhs patterns.

-> ListT TCM SplitProblem 

Split a problem at the first constructor pattern which is actually of datatype type.

Or, if there is no constructor pattern left and the rest type is a record type and the first rest pattern is a projection pattern, split the rest type.

Implicit patterns should have been inserted.