14.6 Coercions and Pretty-Printing
14.6 Coercions and Pretty-Printing
To every declared coercion f, we automatically define an
associated pretty-printing rule, also named f, to hide the coercion
applications. Thus (f t1..tn t) is printed as t where n is the
number of parameters of the source class of f. The user can change
this behaviour just by overwriting the rule f by a new one with the
same name (see chapter 9 for more details about
pretty-printing rules). If f is a coercion to FUNCLASS,
another pretty-printing rule called f1 is also generated. This last
rule prints (f t1..tn tn+1..tm) as (f tn+1..tm).
In the following examples, we changed the coercion pretty-printing
rules to show the inserted coercions.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.5.html at 8/10/98