Struct Array

pub struct Array<'st, X: Sorted<'st>, Y: Sorted<'st>>(/* private fields */);

Representation of a functional array with extensionality. A possibly unbounded container of values of sort Y, indexed by values of sort X.

Trait Implementations

impl<'st, X: Sorted<'st>, Y: Sorted<'st>> Clone for Array<'st, X, Y>

fn clone(&self) -> Self

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'st, X: Debug + Sorted<'st>, Y: Debug + Sorted<'st>> Debug for Array<'st, X, Y>

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

Formats the value using the given formatter.

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

fn from(value: Array<'st, X, Y>) -> Self

Converts to this type from the input type.

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

fn from(t: STerm<'st>) -> Self

Converts to this type from the input type.

impl<'st, X: Sorted<'st>, Y: Sorted<'st>> IntoWithStorage<'st, Array<'st, X, Y>> for Const<'st, Array<'st, X, Y>>

fn into_with_storage(self, _st: &'st Storage) -> Array<'st, X, Y>

Construct a STerm with the presence of Storage

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

const AST_SORT: Sort<'static>

The sort of this sort.

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

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

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

The storage associated with the term.

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.

impl<'st, X: Sorted<'st>, Y: Sorted<'st>> Copy for Array<'st, X, Y>