1

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

4
  • 3
    Check the View -> Display notations menu entry. Oct 4, 2016 at 15:51
  • thank you! i had it checked when i took the screenshots but somehow toggling it fixes it.
    – Falcon
    Oct 4, 2016 at 16:29
  • You should respond unsing the Answer box ;)
    – Vinz
    Oct 5, 2016 at 6:46
  • @Vinz All right. Done :) Oct 5, 2016 at 7:14

1 Answer 1

3

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.

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.