Enum PTerm 

pub enum PTerm {
    Ident(String),
    App(Box<PTerm>, Vec<PTerm>),
    Tuple(Vec<PTerm>),
    Hole,
    Op(&'static str, Box<PTerm>, Box<PTerm>),
}

A term as a proof SCRIPT writes it — the argument of exact, have, refine, use.

One syntax serves two languages, because Lean’s does: the same ⟨a, b⟩ is a conjunction proof against p ∧ q and a witness-and-proof pair against ∃x. φ, and the same bare name is a hypothesis in a proof position and a variable in a value position. Which language a term is read in is decided by the position, never by the term (ProofState::exact_term checks it as a proof, ProofState::value_term as a value).

Variants

Ident(String)

A bare name: a hypothesis, a bound variable, or a constant.

App(Box<PTerm>, Vec<PTerm>)

Juxtaposition — f a b. Modus ponens over an implication, instantiation over a universal, a function application in a value position.

Tuple(Vec<PTerm>)

The anonymous constructor (a, b) / ⟨a, b⟩.

Hole

A ?_ / ?name hole — a subgoal under refine, and an error anywhere else.

Op(&'static str, Box<PTerm>, Box<PTerm>)

An infix arithmetic operator, by its ProofTerm function name (add/sub/mul).

Trait Implementations

impl Clone for PTerm

fn clone(&self) -> PTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PTerm

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

Formats the value using the given formatter.

impl PartialEq for PTerm

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for PTerm