Struct Declared 

pub struct Declared(/* private fields */);

Represent a specific function (or constant, or sort) declared in a Solver.

Declared is an opaque shared reference to a Declaration declared in a Solver. The only way to obtain a Declared is through Solver::declare(). Declared derefs to the underlying Declaration to immutably access its fields.

Comparison of Declared objects is nominal, that is, equality and hashing operate on the identity of the objects, not on their values. In other words, two Declared objects with exactly the same fields (and in particular the same name), created by two different calls to Solver::declare() will compare different and have a possibly different hash. Moreover, cloning a Declared object is a cheap operation and produces a second object which compares equal to the first. Under the hood, this is the behavior of Nominal<Arc<Declaration>>, so we also refer to the Nominal type for details.

Trait Implementations

impl Clone for Declared

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Declared

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

Formats the value using the given formatter.

impl Deref for Declared

type Target = Nominal<Arc<Declaration<Sort, Sort>>>

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl Eq for Declared

impl From<Declared> for Function

fn from(val: Declared) -> Self

Converts to this type from the input type.

impl From<Declared> for UserFunction

fn from(value: Declared) -> Self

Converts to this type from the input type.

impl From<Declared> for SortHead

fn from(val: Declared) -> Self

Converts to this type from the input type.

impl From<Declared> for FunctionRef

fn from(val: Declared) -> Self

Converts to this type from the input type.

impl From<Declared> for Atom

fn from(val: Declared) -> Self

Converts to this type from the input type.

impl Hash for Declared

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 Located for Declared

fn span(&self) -> Option<Span>

Gets the Span tracked by the type.

impl PartialEq for Declared

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Resolve for Declared

fn resolve(&self, _env: &Env, _pool: &dyn TermPool, _role: Role) -> Result<Self>

Perform name resolution on self.

impl StructuralPartialEq for Declared

impl ToTerm for Declared

fn into_term_in(self, pool: &dyn TermPool) -> Term

Convert the object into a Term by uniquing in the given TermPool.

fn to_term_in(&self, pool: &dyn TermPool) -> Term

Convert the object (by reference) into a Term by uniquing in the given TermPool.

impl TypeCheck for Declared

fn type_check(&self) -> Result<Sort>