11. EasyCrypt Proof General
| 11.1 EasyCrypt specific commands | ||
| 11.2 EasyCrypt weak-check mode | ||
| 11.3 EasyCrypt customizations |
EasyCrypt Proof General is an instantiation of Proof General for the EasyCrypt proof assistant.
11.1 EasyCrypt specific commands
EasyCrypt Proof General supplies the following key-bindings:
- C-c C-a C-p
Prompts for “print” query arguments.
- C-c C-a C-c
The same for a “check” query.
11.2 EasyCrypt weak-check mode
The EasyCrypt menu contains a Weak-check mode toggle menu, which
allows you to enable or disable the EasyCrypt Weak-Check mode. When
enabled, all smt calls are ignored and assumed to succeed.
11.3 EasyCrypt customizations
Here are some of the other user options specific to EasyCrypt. You can set these as usual with the customization mechanism.
- User Option: easycrypt-prog-name
Name of program to run EasyCrypt.
The default value is
"easycrypt".
- Variable: easycrypt-load-path
Non-standard EasyCrypt library load path.
This list specifies the include path for EasyCrypt. The elements of this list are strings.
This document was generated on November 21, 2024 using texi2html 1.82.