Attribute Macro vstd::prelude::verus_enum_synthesize

#[verus_enum_synthesize]