Macro prusti_contracts::ghost

source · 
ghost!() { /* proc-macro */ }
Expand description

A macro for defining ghost blocks which will be left in for verification but omitted during compilation.