Enum ExprKind 

pub enum ExprKind {
    Implies(Box<Expr>, Box<Expr>),
    Or(Box<Expr>, Box<Expr>),
    And(Box<Expr>, Box<Expr>),
    Not(Box<Expr>),
    Compare {
        left: Box<Expr>,
        op: CmpOp,
        right: Box<Expr>,
    },
    Arithmetic {
        left: Box<Expr>,
        op: ArithOp,
        right: Box<Expr>,
    },
    Old(Box<Expr>),
    Quantifier {
        kind: QuantifierKind,
        binding: String,
        ty: String,
        body: Box<Expr>,
    },
    Call {
        name: String,
        args: Vec<CallArg>,
    },
    FieldAccess {
        root: Box<Expr>,
        fields: Vec<String>,
    },
    List(Vec<Expr>),
    Ident(String),
    Literal(Literal),
}

Expression variants.

Variants

Implies(Box<Expr>, Box<Expr>)

a => b — logical implication.

Or(Box<Expr>, Box<Expr>)

a || b

And(Box<Expr>, Box<Expr>)

a && b

Not(Box<Expr>)

!a

Compare

a == b, a > b, etc.

Fields

left: Box<Expr>

op: CmpOp

right: Box<Expr>

Arithmetic

a + b, a - b

Fields

left: Box<Expr>

op: ArithOp

right: Box<Expr>

Old(Box<Expr>)

old(expr) — pre-state reference.

Quantifier

forall x: T => body or exists x: T => body

Fields

kind: QuantifierKind

binding: String

ty: String

body: Box<Expr>

Call

name(args) — function call.

Fields

name: String

args: Vec<CallArg>

FieldAccess

Field access chain: a.b.c or f(x).y.z. root is the base expression, fields are the .-accessed names.

Fields

root: Box<Expr>

fields: Vec<String>

List(Vec<Expr>)

List literal: [a, b, c].

Ident(String)

A plain identifier: amount, Active, email.

Literal(Literal)

A literal value.

Trait Implementations

impl Clone for ExprKind

fn clone(&self) -> ExprKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExprKind

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

Formats the value using the given formatter.

impl Serialize for ExprKind

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

where __S: Serializer,

Serialize this value into the given Serde serializer.