The iteration attributes control choice of display form definition based on immediately-nested occurrences of the same term. The idea is to group occurrences into iteration families . An iteration family has a head display form definition and one or more tail definitions. A tail definition can only be used as an immediate subterm of a head in the same family or another tail in the same family. Choice of display form is also affected by the use of the iterate variable # as the id of a term slot format. If # is used in some term slot of a definition, then the definition is only usable if the same term occurs in the subterm slot that uses the #.
An example should make this clearer. Say we want a set of display forms
for
abstraction
terms such that the
character is
suppressed on nested occurrences. The following definitions would work:
<x:var>.<t:term:E>== lambda(<x>.<t>)
;;
#Hd A ::
<x:var>,<#:term:E>== lambda(<x>.<#>) ;;
#Tl A ::<x:var>.<t:term:E>== lambda(<x>.<t>) ;;
#Tl A ::<x:var>,<#:term:E>== lambda(<x>.<#>) ;;
Using these the term lambda(x.lambda(y.lambda(z.x))) would be displayed as:
x,y,z.x