| #
26df0c04 |
|
03-May-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Replace subseq->match abbreviation.
The subseq_abbreviation mechanism was a useful way of quoting some of a
definition or term, specialised to the case of left-associated sequences.
Lambda abstractions are now handled better.
The previous subseq mechanism required some generalisations. It is now replaced
by match_abbreviation, which is a more general approach.
The match mechanism picks a term, can select a matching subterm, and can
rewrite the selected term based on pattern matching also. The new mechanism
can cover all the cases of the previous one, as shown in examples.
|