Struct AuthViewRel 

pub struct AuthViewRel<T>(/* private fields */);

The relation that specifies Auth.

Trait Implementations

impl<T: UnitRA> ViewRel for AuthViewRel<T>

fn rel(a: Option<T>, f: T) -> bool

(open)

match a {
    Some(a) => f.incl(a),
    None => true,
}

fn rel_mono(a: Option<T>, f1: T, f2: T)

(law)

requires

Self::rel(a, f1)

requires

f2.incl(f1)

ensures

Self::rel(a, f2)

fn rel_none(a: Option<T>, f: T)

(law)

ensures

Self::rel(None, f)

fn rel_unit(a: Option<T>)

(law)

ensures

Self::rel(a, T::unit())

type Auth = T

The type of the authority portion of a view

type Frag = T

The type of a fragment portion of a view