pub trait ImputeConstantDomain: Domain {
    type Imputed;

    // Required method
    fn impute_constant<'a>(
        default: &'a Self::Carrier,
        constant: &'a Self::Imputed
    ) -> &'a Self::Imputed;
}
Expand description

Utility trait to impute with a constant, regardless of the representation of nullity.

Required Associated Types§

source

type Imputed

This is the type of Self::Carrier after imputation.

On any type D for which the ImputeConstantDomain trait is implemented, the syntax D::Imputed refers to this associated type. For example, consider D to be OptionDomain<T>, the domain of all Option<T>. The implementation of this trait for OptionDomain<T> designates that type Imputed = T. Thus OptionDomain<T>::Imputed is T.

Proof Definition

Self::Imputed can represent the set of possible output values after imputation.

Required Methods§

source

fn impute_constant<'a>( default: &'a Self::Carrier, constant: &'a Self::Imputed ) -> &'a Self::Imputed

A function that replaces a potentially-null carrier type with a non-null imputed type.

Proof Definition

For any setting of the input parameters, where constant is non-null, the function returns a non-null value.

Implementors§