Macro vstd::prelude::verus_proof_expr

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