TVar package:Agda
Type used when numbering pattern variables.
Label the pattern variables from left to right using one label for
each variable pattern and one for each dot pattern.
Augment pattern variables with their de Bruijn index.
Intended, but unpractical due to the absence of type-level lambda, is:
labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern'
(i,x)))
intersectVars us vs checks whether all relevant elements in
us and vs are variables, and if yes, returns a prune
list which says True for arguments which are different and
can be pruned.
For each variable in the patterns of a split clause, we remember the
de Bruijn-index and the literals excluded by previous matches.
Collect all relevant free variables, excluding the "unused" ones.