## 11 EasyCrypt Proof General

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.

Variable: easycrypt-web-page ¶

  URL of web page for EasyCrypt.