Trait StaticSorted

pub trait StaticSorted<'st>: Into<STerm<'st>> + From<STerm<'st>> {
    type Inner: StaticSorted<'st>;

    const AST_SORT: Sort<'static>;

    // Required method
    fn static_st(&self) -> &'st Storage;

    // Provided methods
    fn sort() -> Sort<'st> { ... }
    fn new_const(st: &'st Storage, name: &str) -> Const<'st, Self> { ... }
}

A trait for statically typing STM-LIB terms.

Refer to the Sorted trait for a more general version of this trait.

Required Associated Constants

const AST_SORT: Sort<'static>

The sort of this sort.

Required Associated Types

type Inner: StaticSorted<'st>

The inner type of the term. This is used for Const<'st, T> where the inner type is T.

Required Methods

fn static_st(&self) -> &'st Storage

The storage associated with the term.

Provided Methods

fn sort() -> Sort<'st>

The sort of this sort.

fn new_const(st: &'st Storage, name: &str) -> Const<'st, Self>

Construct a new constante of this sort.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<'st> StaticSorted<'st> for Bool<'st>

const AST_SORT: Sort<'static>

type Inner = Bool<'st>

impl<'st> StaticSorted<'st> for Int<'st>

const AST_SORT: Sort<'static>

type Inner = Int<'st>

impl<'st> StaticSorted<'st> for Real<'st>

const AST_SORT: Sort<'static>

type Inner = Real<'st>

impl<'st, X, Y> StaticSorted<'st> for Array<'st, X, Y>

where X: StaticSorted<'st>, Y: StaticSorted<'st>,

const AST_SORT: Sort<'static>

type Inner = Array<'st, X, Y>

impl<'st, const M: usize> StaticSorted<'st> for BitVec<'st, M>

const AST_SORT: Sort<'static>

type Inner = BitVec<'st, M>