Module lean

hax_lib::proc_macros

Module lean

Expand description

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

Macros§

prop: The Prop version of lean_expr.

Attribute Macros§

after: This macro inlines verbatim lean code before a Rust item.
before: This macro inlines verbatim lean code before a Rust item.
replace: Replaces a Rust item with some verbatim lean code.
replace_body: Replaces the body of a Rust function with some verbatim lean code.