14. EasyCrypt Proof General
|14.1 EasyCrypt specific commands|
|14.2 EasyCrypt weak-check mode|
|14.3 EasyCrypt customizations|
EasyCrypt Proof General is an instantiation of Proof General for the EasyCrypt proof assistant.
14.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.
14.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
smt calls are ignored and assumed to succeed.
14.3 EasyCrypt customizations
Here are some of the other user options specific to EasyCrypt. You can set these as usual with the customization mechanism.
- Variable: easycrypt-load-path
Non-standard EasyCrypt library load path. This list specifies the include path for EasyCrypt.
This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.