The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

  Dear Ewen,

> Can the pretty-printing mechanism be changed to prevent `unnecessary'
> types being shown?

  A rule for Coq output is that what is printed could be re-parsed as
is. Then, you can avoid `unnecessary' types being shown if a dual
mechanism allow to automatically deduce these types.

> For example, it is often difficult to read terms like
> 
> pair bigtype1 bigtype2 a b
> 
> when what you're really interested in is "pair a b".

  Concerning, the "prod" type introduced by the "pair" constructor, there is
already a built-in notation avoiding the types :

Coq < Check (pair nat nat O O).
(O,O)
     : nat*nat

Coq < Check (O,O).
(O,O)
     : nat*nat

  For the general case, there are 2 solutions. The nicer one is to use
the "Implicit Arguments On" directive. Then arguments that are "easy"
to infer must not be written nor are they printed. Example extracted
from file theories/LISTS/PolyList :

Coq < Implicit Arguments On.
Coq < Inductive list : Set := nil : list | cons : A -> list -> list.
Coq < Check (cons O (nil nat)).
Check (cons O (nil nat)).
(cons O (nil nat))
     : (list nat)

  ... you don't have to give the type of "O" for "cons" (but still
  for "nil" since, taking it alone, there is no mean to know an empty
  list of what)

  The second solution is to give a pretty-printing rule. Example
extracted from theories/INIT/DatatypesSyntax (available by default
at toplevel):

Coq < Syntax constr
        level 1:
          fst_imp [<<(fst $_ $_ $t2)>>] -> [ [<hov 0> "(Fst " $t2:E ")"] ].
Coq < Check (fst nat nat (O,O)).
(Fst (O,O))
     : nat

  But then, you'd like to have the notation "Fst (O,O))" parsed. For
that, you need to declare a "Syntactic Definition" as follows:

Coq < Syntactic Definition Fst := (fst ? ?).
Coq < Check (Fst (O,O)).
(Fst (O,O))
     : nat

  Note that in this latter case, you have to invent a new identifier.

  All of this is in section 2.6 of the reference manual.

  Best regards,
                                                  Hugo herbelin