Macro verus_ghost_inv_macro_exprs 

verus_ghost_inv_macro_exprs!() { /* proc-macro */ }