Struct UntranslatedGoal 

pub struct UntranslatedGoal {
    pub givens: Vec<(String, String)>,
    pub premises: Vec<Spanned<Expr>>,
    pub claim: (Spanned<Expr>, Spanned<Expr>),
}

A goal un-translated back to Aver-space: the ∀-binders split into data GIVENS (name + Aver type name) and PROP premises (surviving hypotheses, e.g. an induction hypothesis, rendered as Aver Bool expressions for when), plus the equality CLAIM (lhs, rhs).

Fields

givens: Vec<(String, String)>

(binder name, Aver type name) for each data ∀-binder — the law’s givens.

premises: Vec<Spanned<Expr>>

Surviving hypothesis binders as Aver Bool expressions — the law’s when premises.

claim: (Spanned<Expr>, Spanned<Expr>)

The equality claim (lhs, rhs).

Trait Implementations

impl Clone for UntranslatedGoal

fn clone(&self) -> UntranslatedGoal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UntranslatedGoal

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

Formats the value using the given formatter.