The term <"a","b">.1 is an abstract redex. It contracts to the term "a".
The basic conversion for contracting both primitive and abstract redices is AbRedexC. Abstract redices are added to a table that AbRedexC accesses using the function
where id is the opid of the outermost term of the redex, and c is a direct-computation conversion for contracting instances of the redex. Note that if the outermost term is an apply term, then the id is taken from the term at the head of the possibly-iterated application.
Instances of add_AbReduce_conv are usually included in ML objects positioned immediately after the definitions of non-canonical abstractions. For example, the declaration of the redex for the pi1 term could be
An alternative method for indicating an abstract redex is to associate a `reducible' attribute with an abstract non-canonical term. The AbRedexC conversion on being applied to a term first unfolds all reducible abstractions at the top level of the term tree before further analyzing the term to see if it is a redex. When this method is applicable, it is more concise than using add_Reduce_conv. A reducible attribute is associated with a term using the function
It takes as its token argument the opid of the term.