Struct AdtSortVariant

pub struct AdtSortVariant {
    field_names: Vec<Symbol>,
    sorts: List<Sort>,
}

Fields

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.

Implementations

impl AdtSortVariant

pub fn new(fields: Vec<(Symbol, Sort)>) -> Self

pub fn fields(&self) -> usize

pub fn field_names(&self) -> &Vec<Symbol>

pub fn sort_by_field_name(&self, args: &[Sort]) -> FxIndexMap<Symbol, Sort>

pub fn field_by_name( &self, def_id: DefId, args: &[Sort], name: Symbol, ) -> Option<(FieldProj, Sort)>

pub fn field_sorts(&self, args: &[Sort]) -> List<Sort>

Trait Implementations

impl Debug for AdtSortVariant

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

Formats the value using the given formatter.

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

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

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

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

impl Hash for AdtSortVariant

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 PartialEq for AdtSortVariant

fn eq(&self, other: &AdtSortVariant) -> 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 AdtSortVariant

impl StructuralPartialEq for AdtSortVariant