vstd::prelude

Macro verus_keep_ghost

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