Enum AttrPayload

pub enum AttrPayload {
    ItemStatus(ItemStatus),
    AssociatedItem {
        role: AssociationRole,
        item: ItemUid,
    },
    Uid(ItemUid),
    ItemQuote(ItemQuote),
    NeverErased,
    NewtypeAsRefinement,
    Lemma,
    Language,
    ProcessRead,
    ProcessWrite,
    ProcessInit,
    ProtocolMessages,
    PVConstructor,
    PVHandwritten,
    TraitMethodNoPrePost,
    Erased,
    Order(i32),
}

Hax only understands one attribute: #[hax::json(PAYLOAD)] where PAYLOAD is a JSON serialization of an inhabitant of AttrPayload.

Variants

ItemStatus(ItemStatus)

AssociatedItem

Mark an item as associated with another one

Fields

role: AssociationRole

What is the nature of the association?

item: ItemUid

What is the identifier of the target item?

Uid(ItemUid)

ItemQuote(ItemQuote)

Decides of the position of a item quote

NeverErased

Mark an item so that hax never drop its body (this is useful for pre- and post- conditions of a function we dropped the body of: pre and post are part of type signature)

NewtypeAsRefinement

Lemma

Mark an item as a lemma statement to prove in the backend

Language

ProcessRead

ProcessWrite

ProcessInit

ProtocolMessages

PVConstructor

PVHandwritten

TraitMethodNoPrePost

Erased

Make an item opaque

Order(i32)

In the context of a set of fields (e.g. on a struct), overrides its order. By default, the order of a field is its index, e.g. the first field has order 0, the i-th field has order i+1. Rust fields order matters: it rules how bits are represented. Once extracted, the order matters, but for different reasons, e.g. a field is refined with another, requiring a specific order.

Trait Implementations

impl Clone for AttrPayload

fn clone(&self) -> AttrPayload

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AttrPayload

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for AttrPayload

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl From<&AttrPayload> for TokenStream

fn from(payload: &AttrPayload) -> Self

Converts to this type from the input type.

impl Serialize for AttrPayload

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl ToTokens for AttrPayload

fn to_tokens(&self, tokens: &mut TokenStream)

Write self to the given TokenStream.

fn to_token_stream(&self) -> TokenStream

Convert self directly into a TokenStream object.

fn into_token_stream(self) -> TokenStream

where Self: Sized,

Convert self directly into a TokenStream object.