Struct RefinementValue 

pub struct RefinementValue<T: Clone> { /* private fields */ }

A refinement-type value: a value together with a dynamically-checked proof tag. The proof is stored as a bool result from a predicate closure so the type can be constructed and inspected without heavyweight theorem-prover plumbing.

Implementations

impl<T: Clone> RefinementValue<T>

pub fn new( value: T, predicate_name: impl Into<String>, predicate: impl Fn(&T) -> bool, ) -> Self

Construct a refinement value, evaluating the predicate immediately.

pub fn val(&self) -> &T

Return a reference to the underlying value.

pub fn is_valid(&self) -> bool

Return whether the predicate holds for this value.

pub fn predicate_name(&self) -> &str

Name of the predicate used to refine this type.

pub fn coerce( &self, new_name: impl Into<String>, implication: impl Fn(&T) -> bool, ) -> RefinementValue<T>

Coerce to a different refinement type given a proof that the new predicate follows from the old one (encoded as a Rust closure for demo purposes).

Trait Implementations

impl<T: Clone + Clone> Clone for RefinementValue<T>

fn clone(&self) -> RefinementValue<T>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Debug + Clone> Debug for RefinementValue<T>

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

Formats the value using the given formatter.