Attribute Macro after

#[after]

This macro inlines verbatim proverif code before a Rust item.

This macro takes a string literal containing backend code. Just as backend expression macros, this literal can contains dollar-prefixed Rust names.

Note: when targetting F*, you can prepend a first comma-separated argument: interface, impl or both. This controls where the code will apprear: in the fst or fsti files or both.