pub trait Domain: Clone + PartialEq + Debug + Send + Sync {
type Carrier;
// Required method
fn member(&self, val: &Self::Carrier) -> Fallible<bool>;
}
Expand description
Required Associated Types§
sourcetype Carrier
type Carrier
The underlying type that the Domain specializes. This is the type of a member of a domain, where a domain is any data type that implements this trait.
On any type D
for which the Domain
trait is implemented,
the syntax D::Carrier
refers to this associated type.
For example, consider D
to be AtomDomain<T>
, the domain of all non-null values of type T
.
The implementation of this trait for AtomDomain<T>
designates that type Carrier = T
.
Thus AtomDomain<T>::Carrier
is T
.
§Proof Definition
Self::Carrier
can represent all values in the set described by Self
.
Required Methods§
sourcefn member(&self, val: &Self::Carrier) -> Fallible<bool>
fn member(&self, val: &Self::Carrier) -> Fallible<bool>
Predicate to test an element for membership in the domain.
Not all possible values of ::Carrier
are a member of the domain.
§Proof Definition
For all settings of the input parameters,
returns Err(e)
if the member check failed,
or Ok(out)
, where out
is true if val
is a member of self
, otherwise false.
§Notes
It generally suffices to treat Err(e)
as if val
is not a member of the domain.
It can be useful, however, to see richer debug information via e
in the event of a failure.