Module fstar

Procedular macros that have an effect only for the backend fstar.

Macros

prop

The Prop version of fstar_expr.

Attribute Macros

after

This macro inlines verbatim fstar code before a Rust item.

before

This macro inlines verbatim fstar code before a Rust item.

options

When extracting to F*, wrap this item in #push-options "..." and #pop-options.

postprocess_with

Postprocess an item with a given tactic. This macro takes the tactic in parameter: this may be a Rust identifier or a raw snippet of F* code as a string literal.

replace

Replaces a Rust item with some verbatim fstar code.

replace_body

Replaces the body of a Rust function with some verbatim fstar code.

smt_pat

Allows to add SMT patterns to a lemma. For more informations about SMT patterns, please take a look here: https://fstar-lang.org/tutorial/book/under_the_hood/uth_smt.html#designing-a-library-with-smt-patterns.

verification_status

When extracting to F*, inform about what is the current verification status for an item. It can either be lax or panic_free.