Agda.TypeChecking.RecordPatterns

Code which replaces pattern matching on record constructors with uses of projection functions.

Documentation

translateRecordPatterns :: Clause -> TCM Clause

Replaces pattern matching on record constructors with uses of projection functions. Does not remove record constructor patterns which have sub-patterns containing non-record constructor or literal patterns.

If the input clause contains dot patterns inside record patterns, then the translation may yield clauses which are not type-correct. However, we believe that it is safe to use the output as input to compileClauses. Perhaps it would be better to perform record pattern translation on the compiled clauses instead, but the code below has already been implemented and seems to work.