[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

14. EasyCrypt Proof General

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 enabled, all 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.

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.

[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated by Erik Martin-Dorel on August 21, 2021 using texi2html 1.82.