Struct AdtSortDefData

struct AdtSortDefData {
    def_id: DefId,
    params: Vec<ParamTy>,
    field_names: Vec<Symbol>,
    sorts: List<Sort>,
}

Fields

def_id: DefId

DefId of the struct, enum or type aliases this data sort is associated to

params: Vec<ParamTy>

The list of the type parameters used in the #[flux::refined_by(..)] annotation.

See fhir::RefinedBy::sort_params for more details. This is a version of that but using ParamTy instead of DefId.

The length of this list corresponds to the number of sort variables bound by this definition.

field_names: Vec<Symbol>

The list of field names as declared in the #[flux::refined_by(...)] annotation

sorts: List<Sort>

The sort of each of the fields. Note that these can contain sort variables. Methods used to access these sorts guarantee they are properly instantiated.

Trait Implementations

impl Debug for AdtSortDefData

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

Formats the value using the given formatter.

impl<__D: TyDecoder> Decodable<__D> for AdtSortDefData

fn decode(__decoder: &mut __D) -> Self

impl<__E: TyEncoder> Encodable<__E> for AdtSortDefData

fn encode(&self, __encoder: &mut __E)

impl Hash for AdtSortDefData

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Internable for AdtSortDefData

fn storage() -> &'static InternStorage<Self>

impl PartialEq for AdtSortDefData

fn eq(&self, other: &AdtSortDefData) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for AdtSortDefData

impl StructuralPartialEq for AdtSortDefData