GitHub

The subset of rust supported by the Lean backend will be similar to F*, the (currently) most mature backend of Hax. This includes basic expressions, enums, structs, traits, etc. Features left out of this milestone (like returning &mut require engine work). This milestone does not cover the extension of the Lean library

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Lean backend v1.0

[Lean] Handle pre/post conditions, generate lemmas

Rust Engine: Name Rendering: support <code>GlobalId</code> suffixes

[Lean] Extend support for associated types

[Lean] Add support for constant generic parameters

[Lean] : support mutual dependencies (between items, between modules, inside traits/impl)

[Lean] Advanced pattern-matching

[Lean] Arrays with non-integer-literal size

[Rust-engine/engine] Some errors are not displayed in the CLI

[Lean] Split output in several files

[Lean] Name-rendering should strip the prefix of the current file

[Lean] Support explicit impl expressions

[Lean] Support captured variables in closures

[Lean] Add a resugaring for type definitions, splitting Enums, Structs and Unions

[Lean] Add support for <code>dyn</code>

[Lean] Print opaque types

[Lean] Incorrect treatment of trait-level parameters

Lean backend v1.0

List view