Macro vstd::prelude::verus_exec_expr_erase_ghost

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