Search code examples
coqcoqide

How to change display style in Coq IDE to match Coqtop?

The implication connective is printed as lambda expression in my coqide (OS X El Capitan). is that the expected behavior? I would prefer to see them printed as in coqtop. I couldn't find the option/command line option to change the display style.

coqtop and coqide

Solution

  • Short answer

    Make sure the View → Display notations menu entry is checked in CoqIDE.

    Long answer

    Coq by default pretty-prints stuff using notations.

    A notation is a symbolic abbreviation denoting some term or term pattern.

    The notation for -> is defined in Coq.Init.Logic:

    Notation "A -> B" := (forall (_ : A), B) : type_scope.

    At this point we can conclude that Coq for some reason is unfolding notations for you.

    In 'coqtop' (a toplevel, or REPL for Coq) or in ProofGeneral you can use the Vernacular commands

    Set Printing Notations.

    and

    Unset Printing Notations.

    in your proof scripts to control the output (one can read Set / Unset in the commands above as Use / Do not use).

    Unfortunately, those do not work in CoqIDE v8.5: if you try it, you'll get the following error message:

    This will not work. Use CoqIDE display menu instead

    I guess the only reasonable option we have is to check the View → Display notations menu entry.