vstd::prelude

Macro verus_erase_ghost

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