Trait rsmt2::print::AdtVariantField

source · [−]
pub trait AdtVariantField {
    type FieldSym: Sym2Smt;
    type FieldSort: Sort2Smt;

    fn field_sym(&self) -> &Self::FieldSym;
    fn field_sort(&self) -> &Self::FieldSort;
}
Expand description

Contains data for a field of a variant of an ADT.

  • Used by AdtVariant.
  • T: AdtVariantField ⇒ &T: AdtVariantField

Implementing this trait for you own types is totally fine but if you don’t, you can use pairs (impl Sym2Smt, impl Sort2Smt) which implement this trait. See examples.

Examples

use rsmt2::print::*;

let field = ("impl Sym2Smt", "impl Sort2Smt");
let _ = field.field_sym();
let _ = field.field_sort();

fn test(_: impl AdtVariantField) {}
test(&field);
test(field);

Required Associated Types

Field symbol (name).

Field sort.

Required Methods

Field symbol accessor.

Field sort accessor.

Implementations on Foreign Types

Implementors