Enum Syn 

pub enum Syn {
    Lit(i64),
    Var(i64),
    Name(String),
    App(Box<Syn>, Box<Syn>),
}

The object language’s four shapes, as this module reads them.

The reflection grammar the tactic primitives are handed is SLit n, SVar i, SName s and SApp f x — four global constructors applied to literals and to each other. That is the whole of it. Reading it here rather than through the kernel’s reify extractors is the point: a shared reader is a shared assumption, and an assumption both kernels make is one neither checks.

Variants

Lit(i64)

SLit n — an integer literal of the object language.

Var(i64)

SVar i — a de Bruijn occurrence.

Name(String)

SName s — a named global: a free variable to arithmetic, a function symbol to congruence.

App(Box<Syn>, Box<Syn>)

SApp f x — object-language application, curried.

Trait Implementations

impl Clone for Syn

fn clone(&self) -> Syn

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Syn

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

Formats the value using the given formatter.

impl PartialEq for Syn

fn eq(&self, other: &Syn) -> 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 Eq for Syn

impl StructuralPartialEq for Syn