[ << ] [ >> ] [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.

Variable: easycrypt-prog-name

Name of program to run EasyCrypt.

Variable: easycrypt-load-path

Non-standard EasyCrypt library load path. This list specifies the include path for EasyCrypt.

Variable: easycrypt-web-page

URL of web page for EasyCrypt.


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

This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.