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