Enum Op 

pub enum Op {
    Implies,
    Equiv,
    Or,
    And,
    Eq,
    Neq,
    Lt,
    Gt,
    Le,
    Ge,
    In,
    NotIn,
    Subseteq,
    Supseteq,
    AtAt,
    OneTo,
    Cup,
    Cap,
    SetMinus,
    DotDot,
    Plus,
    Minus,
    Times,
    Div,
    Mod,
    Cartesian,
    Concat,
    Pow,
    Not,
    Always,
    Eventually,
    Forall,
    Exists,
    Domain,
    Subset,
    BigUnion,
    Enabled,
    Unchanged,
    LeadsTo,
    TemporalForall,
    TemporalExists,
    User(&'static str),
}

Variants

Implies

Equiv

Or

And

Eq

Neq

Lt

Gt

Le

Ge

In

NotIn

Subseteq

Supseteq

AtAt

OneTo

Cup

Cap

SetMinus

DotDot

Plus

Minus

Times

Div

Mod

Cartesian

Concat

Pow

Not

Always

Eventually

Forall

Exists

Domain

Subset

BigUnion

Enabled

Unchanged

LeadsTo

P ~> Q: temporal leads-to.

TemporalForall

\AA x : F and \EE x : F: quantification over a hidden variable.

TemporalExists

User(&'static str)

An operator the language reserves a symbol and a precedence for but gives no meaning to. Every one of these exists to be defined by a specification; \prec, \oplus and & are all of them.

Implementations

impl Op

pub fn infix_prec(self) -> Option<u8>

Binding power as an infix operator; None for prefix-only operators.

Ordering follows TLA+’s table where it matters for these specs: \cup binds tighter than =, and :> tighter than @@, so a \cup {b} = c and ("k" :> v) @@ rest parse without parentheses.

pub fn is_postfix(self) -> bool

s^+, s^* and s^# follow their operand rather than sitting between two, so they are never infix.

pub fn is_right_assoc(self) -> bool

pub fn symbol(self) -> &'static str

How the operator is written. Where TLA+ offers several spellings the ASCII one is chosen, so printed output can be re-read by the parser.

pub fn prefix_prec(self) -> u8

How tightly the operator holds its operand when used as a prefix, and so how tightly it binds as a node in printed output.

pub fn is_word(self) -> bool

True for the word-shaped prefix operators, which need a space before their operand where the symbolic ones do not.

Trait Implementations

impl Clone for Op

fn clone(&self) -> Op

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for Op

impl Debug for Op

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

Formats the value using the given formatter.

impl Eq for Op

impl PartialEq for Op

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Op