Add tentative auto-generated EasyCrypt language documentation#976
Add tentative auto-generated EasyCrypt language documentation#976
Conversation
Add two new flags for the `easycrypt` CLI to support LLM coding agents: - `-upto <pos>`: compile up to a given position and print goals there - `-lastgoals`: print the last unproven goals Also add a dedicated `llm` command mode and an LLM agent guide (doc/llm/CLAUDE.md) documenting EasyCrypt tactics and workflow for use with AI coding assistants.
This is a first draft covering: types, operators, predicates, expressions, formulas, programs, modules, module types, theories, sections, cloning, hints, printing, and standard library tour.
|
Of course, it has to be reviewed, extended, amended, etc, etc... but this gives a basis. |
fdupress
left a comment
fdupress
left a comment
There was a problem hiding this comment.
partial review; not meant to be human-consumed :)
|
|
||
| require import AllCore. | ||
|
|
||
| (* An abstract type with decidable equality *) |
There was a problem hiding this comment.
Probably not an ideal comment here.
| File structure | ||
| ------------------------------------------------------------------------ | ||
|
|
||
| An EasyCrypt source file has the extension ``.ec``. A file consists of |
There was a problem hiding this comment.
EasyCrypt source files can also have the extension .eca for abstract theories. (Add a cross-ref to relevant section?)
| require import AllCore List FSet. | ||
|
|
||
| The ``import`` and ``export`` keywords can also be used standalone to | ||
| import or export a theory that has already been required: |
There was a problem hiding this comment.
Explain/Given an example to show that this can be used to import theories without importing their parent theory?
| scope (defined in the ``Pervasive`` prelude). | ||
|
|
||
| ``unit`` | ||
| The unit type. It has a single value, written ``tt``. It is used |
There was a problem hiding this comment.
tt is also often displayed as ()
|
|
||
| All types in EasyCrypt are *inhabited*: there is a polymorphic | ||
| constant ``witness : 'a`` that provides a default value for any type. | ||
| This means there is no empty type. |
There was a problem hiding this comment.
The witness value is never specified: you will be unable to prove that it is equal to (or different from) any other value in the same type. To extend a type with a distinguished symbol (typically denoted option type constructor is a much better choice.
| ``'a distr`` | ||
| The type of (sub-)distributions over a type ``'a``. A value of | ||
| type ``'a distr`` assigns a probability (a non-negative real) to | ||
| each value of type ``'a``, with the total probability at most 1. |
There was a problem hiding this comment.
This is a parameterized type. (Add a cross-ref to the following section.)
| .. code-block:: easycrypt | ||
|
|
||
| (1, true) (* : int * bool *) | ||
| (1, true, 42) (* : int * bool * int *) |
There was a problem hiding this comment.
The types (t1 * t2) * t3, t1 * (t2 * t3) and t1 * t2 * t3 are isomorphic, but distinct. This is a common source of errors and should be highlighted here.
| Node 1 (Node 2 Leaf Leaf) Leaf. | ||
|
|
||
| Pattern matching is the primary way to inspect algebraic datatypes. | ||
| See :ref:`language-expressions` for the ``match`` expression and |
There was a problem hiding this comment.
Also cross-ref to the match statement?
|
|
||
| .. code-block:: easycrypt | ||
|
|
||
| subtype nat AS Nat = { x : int | 0 <= x }. |
2 participants
This is a first draft covering: types, operators, predicates, expressions, formulas, programs, modules, module types, theories, sections, cloning, hints, printing, and standard library tour.