Enum Expr 

pub enum Expr {
    Num(i64),
    Decimal(String),
    Str(String),
    Bool(bool),
    Ident(String),
    Prime(Box<Expr>),
    At,
    Apply(Box<Expr>, Vec<Expr>),
    FnApply(Box<Expr>, Vec<Expr>),
    Field(Box<Expr>, String),
    Qualified {
        instance: String,
        name: String,
        args: Vec<Expr>,
    },
    Unary(Op, Box<Expr>),
    Binary(Op, Box<Expr>, Box<Expr>),
    Tuple(Vec<Expr>),
    SetEnum(Vec<Expr>),
    SetFilter {
        bound: Box<Bound>,
        pred: Box<Expr>,
    },
    SetMap {
        expr: Box<Expr>,
        bounds: Vec<Bound>,
    },
    Record(Vec<(String, Expr)>),
    RecordSet(Vec<(String, Expr)>),
    FnDef {
        bounds: Vec<Bound>,
        body: Box<Expr>,
    },
    FnSet {
        domain: Box<Expr>,
        range: Box<Expr>,
    },
    Except {
        base: Box<Expr>,
        updates: Vec<(Vec<ExceptPath>, Expr)>,
    },
    Quant {
        kind: QuantKind,
        bounds: Vec<Bound>,
        body: Box<Expr>,
    },
    Choose {
        bound: Box<Bound>,
        body: Box<Expr>,
    },
    Let {
        defs: Vec<Def>,
        instances: Vec<LetInstance>,
        body: Box<Expr>,
    },
    If {
        cond: Box<Expr>,
        then: Box<Expr>,
        otherwise: Box<Expr>,
    },
    Case {
        arms: Vec<(Expr, Expr)>,
        other: Option<Box<Expr>>,
    },
    Lambda {
        params: Vec<Param>,
        body: Box<Expr>,
    },
    ActionBox {
        action: Box<Expr>,
        subscript: Box<Expr>,
    },
    ActionAngle {
        action: Box<Expr>,
        subscript: Box<Expr>,
    },
    Fairness {
        strong: bool,
        subscript: Box<Expr>,
        action: Box<Expr>,
    },
}

Variants

Num(i64)

Decimal(String)

123.456, as written. TLA+ decimals are exact rationals.

Str(String)

Bool(bool)

Ident(String)

Prime(Box<Expr>)

x'

At

@, legal only inside an EXCEPT update.

Apply(Box<Expr>, Vec<Expr>)

Op(a, b) — application of a defined operator.

FnApply(Box<Expr>, Vec<Expr>)

f[a] — function application.

Field(Box<Expr>, String)

r.field

Qualified

Inst!Name(args)

Fields

instance: String

name: String

args: Vec<Expr>

Unary(Op, Box<Expr>)

Binary(Op, Box<Expr>, Box<Expr>)

Tuple(Vec<Expr>)

SetEnum(Vec<Expr>)

SetFilter

{x \in S : P}

Fields

bound: Box<Bound>

pred: Box<Expr>

SetMap

{e : x \in S, y \in T}

Fields

expr: Box<Expr>

bounds: Vec<Bound>

Record(Vec<(String, Expr)>)

[a |-> 1, b |-> 2]

RecordSet(Vec<(String, Expr)>)

[a : S, b : T]

FnDef

[x \in S |-> e]

Fields

bounds: Vec<Bound>

body: Box<Expr>

FnSet

[S -> T]

Fields

domain: Box<Expr>

range: Box<Expr>

Except

[f EXCEPT ![a] = e, !.g = e2]

Fields

base: Box<Expr>

updates: Vec<(Vec<ExceptPath>, Expr)>

Quant

Fields

kind: QuantKind

bounds: Vec<Bound>

body: Box<Expr>

Choose

Fields

bound: Box<Bound>

body: Box<Expr>

Let

Fields

defs: Vec<Def>

instances: Vec<LetInstance>

LET I == INSTANCE M IN ... — an instance whose scope is the body.

body: Box<Expr>

If

Fields

cond: Box<Expr>

then: Box<Expr>

otherwise: Box<Expr>

Case

Fields

arms: Vec<(Expr, Expr)>

other: Option<Box<Expr>>

Lambda

LAMBDA x, y : e — an operator written where one is expected.

Fields

params: Vec<Param>

body: Box<Expr>

ActionBox

[A]_vars

Fields

action: Box<Expr>

subscript: Box<Expr>

ActionAngle

<<A>>_vars

Fields

action: Box<Expr>

subscript: Box<Expr>

Fairness

WF_vars(A) / SF_vars(A)

Fields

strong: bool

subscript: Box<Expr>

action: Box<Expr>

Implementations

impl Expr

pub fn mentions_next_state(&self) -> bool

Does this constrain the successor state? Distinguishes an action’s guard, which says when it may happen, from its effect, which says what it does — the two call for different advice when one of them fails.

pub fn conjunction(items: Vec<Expr>) -> Expr

pub fn disjunction(items: Vec<Expr>) -> Expr

Trait Implementations

impl Clone for Expr

fn clone(&self) -> Expr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Expr

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

Formats the value using the given formatter.

impl Display for Expr

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

Formats the value using the given formatter.

impl Eq for Expr

impl PartialEq for Expr

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Expr