Enum WriteLimit 

pub enum WriteLimit {
    Full,
    Create,
}

What a run may do to a file that already exists inside its write domain (crates/kernel/spec/WriteDomain.lean §8-78).

It narrows the domain and never widens it: the domain answers where a run may write and what kind of file, this answers whether a write may change a file that is already there. Whether the target exists is the filesystem’s fact at the moment of the write, so the check that makes Create hold is the writer’s atomic create; the rule and its refusal are crate::gate::replacing.

Variants

Full

No narrowing beyond the write domain.

Create

Create files that do not exist; change, remove and rename none, including one this run created itself.

Implementations

impl WriteLimit

pub const ALL: [WriteLimit; 2]

Both limits, the one that narrows nothing first.

pub const fn as_str(self) -> &'static str

The word this limit travels under.

Trait Implementations

impl Clone for WriteLimit

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for WriteLimit

impl Debug for WriteLimit

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for WriteLimit

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for WriteLimit

impl Ord for WriteLimit

fn cmp(&self, other: &Self) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

fn clamp_to<R>(self, range: R) -> Self

where Self: Sized, R: ClampBounds<Self>,

🔬This is a nightly-only experimental API. (clamp_to)

Restrict a value to a certain range.

impl PartialEq for WriteLimit

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl PartialOrd for WriteLimit

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Serialize for WriteLimit

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for WriteLimit