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.
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.
- Why does an empty preprocessor command still evaluate to something?
- How to implement variable sized array within C struct
- Character array typecasting to integer
- How can I exclude non-numeric keys? CS50 Caesar Pset2
- How to get the sign, mantissa and exponent of a floating point number
- Why do MCU libraries use logic operations instead of bitfield structs?
- What kind of implementation can I use for a static associative array on a vintage system with very limited resources?
- Determine libraries to link against for a windows library function?
- Passing macro values to arm linker that places variable at a specific location
- running a program with wildcards as arguments
- How to perform addition of two vectors of 8-bit integers with a single addition in C/C++
- GNU RISC-V Embedded GCC throws "x ISA extension `xw' must be set with the versions" error
- Counting pulses using a swiss flow meter with an Arduino, how is it done?
- How to create a folder in C (need to run on both Linux and Windows)
- Is there any way to compute the width of an integer type at compile-time?
- How can I initialize all members of an array to the same value?
- Is C notably faster than C++
- How to get the Windows SDK version number a program is compiling with at compile time
- Confused by difference between expression inside if and expression outside if
- Equivalent of atoi for unsigned integers
- k&r: Exercise 1-18. Program takes input but doesnt produce any output?
- Using in C thrd_sleep() to either wait for time or interrupt by signal. Example?
- How can I compute `exp(x)/2` when `x` is large?
- c programming: answer always equates to 0
- Is it possible to access a parameter of a function from another function in C?
- Will this expression evaluate to true or false (1 or 0) in C?
- What Is the Return Value of strcspn() When Str1 Does not Contain Str2?
- Mapping a numeric range onto another
- Signalled and non-signalled state of event
- Why is faster to do a branch than a lookup?