ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.RecordPatterns

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

valuetranslateCompiledClauses

valuetranslateSplitTree :: SplitTree -> TCM SplitTree

Bottom-up procedure to record-pattern-translate split tree.

valuerecordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]

Take a record pattern p and yield a list of projections corresponding to the pattern variables, from left to right.

E.g. for (x , (y , z)) we return [ fst, fst . snd, snd . snd ].

If it is not a record pattern, error ShouldBeRecordPattern is raised.

valuerecordRHSToCopatterns :: (MonadChange m, PureTCM m) => Clause -> m [Clause]