Macro vstd::prelude::verus

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