Attribute Macro opaque 

#[opaque]

Makes a logical definition or a type declaration opaque, meaning that users of this declaration will not see its definition.

Example

#[opaque]
struct Opaque(()); // This will is an abstract type

#[logic]
#[opaque] // Synonym: #[logic(opaque)]
fn foo() -> i32 { // This is an uninterpreted logic function
    dead
}