Trait dependent_ghost::named::Named

pub trait Named<A>: Sealed {
    type Name;
    fn out_ref(&self) -> &A;
    fn out(self) -> A;
}

A trait describing a value annotated with a type-level name.

While this is most useful alongside the combinators provided by the proof module, names can also be used as a type-level witness that two values are the same. This is useful for things like sorted lists or nonstandard binary maps, where it is important to ensure that the comparison function used is consistent.

This trait has been sealed, as library consumers should not implement this trait for themselves. Instead, see name.

Associated Types

type Name

Loading content...

Required methods

fn out_ref(&self) -> &A

fn out(self) -> A

Loading content...

Implementors

Loading content...