Trait Refinement 

pub trait Refinement {
    type InnerType;

    // Required methods
    fn new(x: Self::InnerType) -> Self;
    fn get(self) -> Self::InnerType;
    fn get_mut(&mut self) -> &mut Self::InnerType;
    fn invariant(value: Self::InnerType) -> Prop;
}

A type that implements Refinement should be a newtype for a type T. The field holding the value of type T should be private, and Refinement should be the only interface to the type.

Please never implement this trait yourself, use the refinement_type macro instead.

Required Associated Types

type InnerType

The base type

Required Methods

fn new(x: Self::InnerType) -> Self

Smart constructor capturing an invariant. Its extraction will yield a proof obligation.

fn get(self) -> Self::InnerType

Destructor for the refined type

fn get_mut(&mut self) -> &mut Self::InnerType

Gets a mutable reference to a refinement

fn invariant(value: Self::InnerType) -> Prop

Tests wether a value satisfies the refinement

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors