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".

Implementors

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

const AST_SORT: Sort<'static>

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

impl<'st, const EB: usize, const SB: usize> StaticSorted<'st> for FloatingPoint<'st, EB, SB>

const AST_SORT: Sort<'static>

type Inner = FloatingPoint<'st, EB, SB>

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

const AST_SORT: Sort<'static>

type Inner = BitVec<'st, M>

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> StaticSorted<'st> for RoundingMode<'st>

const AST_SORT: Sort<'static>

type Inner = RoundingMode<'st>