Enum Unit 

pub enum Unit {
    Constants(Vec<Decl>),
    Variables(Vec<String>),
    Recursive(Vec<Decl>),
    Def(Def),
    Instance {
        name: Option<String>,
        module: String,
        subs: Vec<(String, Expr)>,
    },
    Assume(Expr),
    Theorem(Expr),
    Inner(Box<Module>),
    Opaque,
}

Variants

Constants(Vec<Decl>)

Variables(Vec<String>)

Recursive(Vec<Decl>)

Def(Def)

Instance

S == INSTANCE M WITH x <- e — named when it introduces a prefix, anonymous when the module’s definitions are pulled in directly.

Fields

name: Option<String>

module: String

subs: Vec<(String, Expr)>

Assume(Expr)

Theorem(Expr)

Inner(Box<Module>)

A module declared inside another one.

Opaque

A unit the evaluator has no use for and the parser did not keep: a TLAPS proof, or a theorem stated in the ASSUME ... PROVE form.

Trait Implementations

impl Clone for Unit

fn clone(&self) -> Unit

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Unit

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

Formats the value using the given formatter.

impl Display for Unit

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

Formats the value using the given formatter.

impl Eq for Unit

impl PartialEq for Unit

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Unit