| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
|\ |
|
| |\
| | |
| | | |
compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support
|
| | | |
|
| | | |
|
| | | |
|
| | |\
| | |/
| |/| |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
On the long run, all backends will not have equivalent or equal support
for extraction.
This introduces a function to filter out some Lean-only definitions in
our various arrays of core functions.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Our backend already have support for `isNone`, we just map it and filter
out passing the actual type as it can be inferred via implicit types.
Other backends than Lean are not done in this commit.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In the pure functional model, `swap` is mostly about borrow checking and
should simplify to the pure swap in our backends.
Other backends than Lean are not done in this commit.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
`take` in a pure functional model is the identity function and
everything related to borrow checking is handled by the forward/backward
mechanism.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
|
| | | |
|
|/ / |
|
|\ \
| | |
| | | |
feat(backends/lean): scalars form a linear order
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
More than c1c33de8, actually, scalars form a linear order with a
decidable ≤ operation which is induced by the integer (Z) model.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \ \
| | | |
| | | | |
ci: check code formatting and forbid warnings
|
| | | |
| | | |
| | | | |
Co-authored-by: Son HO <hosonmarc@gmail.com>
|
| | | | |
|
| | | | |
|
|\ \ \ \
| |/ / /
|/| | | |
ci: avoid running duplicate jobs
|
|/ / / |
|
|\ \ \
| | | |
| | | | |
Fix an issue in the loops fixed point
|
| | | | |
|
|/ / / |
|
|\ \ \
| | | |
| | | | |
Ensure we regenerate files properly in CI
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Files that weren't regenerated were marked as not
automatically-generated.
|
|\ \ \ \
| | |/ /
| |/| | |
fix(backends/lean): add a significant amount of keywords
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Taken from
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L33
and
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L36-L43.
This will not extract the tactics.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Taken from
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L12
and sorted.
Tactics are ignored.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
OCD. :D
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | | |
`as` is a reserved keyword and cannot be used as a variable name.
Fixes #139.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \ \
| |_|/
|/| | |
|
| | | |
|
|/ / |
|
|\ \ |
|
| |/
| |
| |
| |
| |
| |
| |
| | |
Not all Nix users can make use of Flakes.
This adds the compatibility for non-Flakes users.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \
| | |
| | | |
Run sanity checks in CI only
|
| | | |
|
|\ \ \
| |_|/
|/| | |
Bump charon
|
|/ / |
|
|\ \
| |/
|/| |
lean: scalars form a preorder
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Via the canonical injection, we can easily define an induced preorder on
scalars and inherit all nice properties.
It's useful to reason on specific scalar preorders w.r.t. Ordering, see
the binary search tree verification example.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \
| |/
|/| |
Fix CI
|
|/ |
|
|\
| |
| | |
Add more definitions to the Lean library
|
| | |
|