Skip to main content

Module attributes

Module attributes 

Source
Expand description

Work with hax attributes.

Structs§

FnLikeAssocatedExpressions
The various linked expressions one can usually find on a (linked or not) function.
LinkedItemGraph
A graph of items connected via the hax attribute AttrPayload::AssociatedItem and UUIDs.
Postcondition
A postcondition.
ProofAttributes
The various linked expressions one can usually find on a (linked or not) function.

Functions§

hax_attributes
Get an iterator over hax attributes contained in the given attributes.
hax_proof_attributes
Get proof attributes attached to the item