Struct ExponentialRules 

pub struct ExponentialRules;

The four rules governing the exponential modality ! in linear logic.

Implementations

impl ExponentialRules

pub fn new() -> Self

Create a new exponential rules structure.

pub fn dereliction(&self, a: &str) -> String

Dereliction: !A ⊢ A (use a resource once).

pub fn contraction(&self, a: &str) -> String

Contraction: !A ⊢ !A ⊗ !A (duplicate a resource).

pub fn weakening(&self, a: &str) -> String

Weakening: !A ⊢ 1 (discard a resource).

pub fn promotion(&self, a: &str, gamma: &[&str]) -> String

Promotion: !Γ ⊢ A → !Γ ⊢ !A (promote to exponential).

pub fn storage(&self, a: &str) -> String

Storage: !A ≡ !A ⊗ !A (idempotency of !).

Trait Implementations

impl Clone for ExponentialRules

fn clone(&self) -> ExponentialRules

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExponentialRules

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

Formats the value using the given formatter.

impl Default for ExponentialRules

fn default() -> ExponentialRules

Returns the “default value” for a type.