Constant move_model::pragmas::EXPORT_ENSURES_PRAGMA

pub const EXPORT_ENSURES_PRAGMA: &str = "export_ensures";

Pragma which indicates that the function’s abort and ensure conditions shall be exported to the verification context even if the implementation of the function is inlined.