hax_lib::proc_macros

Module coq

Expand description

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

Macros§

prop: The Prop version of coq_expr.

Attribute Macros§

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