Struct Conjecture 

pub struct Conjecture {
    pub lhs: TermNode,
    pub rhs: TermNode,
    pub ty: Type,
}

A candidate equation lhs == rhs (both ty-typed) over the shared binders. A conjecture, not a theorem — the charter’s proved-or-dropped gate (VM-filter then kernel proof, 2c–2d) is what turns survivors into usable lemmas.

Fields

lhs: TermNode

rhs: TermNode

ty: Type

Implementations

impl Conjecture

pub fn render(&self, binders: &[Binder]) -> String

Source-shaped rendering, e.g. decode(List.concat(x2, x3)) == List.concat(decode(x2), decode(x3)).

Trait Implementations

impl Clone for Conjecture

fn clone(&self) -> Conjecture

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Conjecture

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

Formats the value using the given formatter.