Attribute Macro builtin
#[builtin]Expand description
This attribute indicates that a logic function or a type should be translated to a specific type in Why3.
#[builtin]This attribute indicates that a logic function or a type should be translated to a specific type in Why3.