Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone






:: Maybe (QName, Type)

Translate record patterns and coverage check with given type?

-> [Clause] 
-> TCM CompiledClauses 

Process function clauses into case tree. This involves: 1. Coverage checking, generating a split tree. 2. Translation of lhs record patterns into rhs uses of projection. Update the split tree. 3. Generating a case tree from the split tree. Phases 1. and 2. are skipped if Nothing.

type Cls = [Cl]Source

nextSplit :: Cls -> Maybe IntSource

Get the index of the next argument we need to split on. This the number of the first pattern that does a match in the first clause.