Struct UntranslateCtx 

pub struct UntranslateCtx {
    pub peano: Option<PeanoCtx>,
}

Context threaded from the --explain render site. peano is set when the law being un-translated has a given whose type is a canonical-Peano ADT (T { Zero; Succ(T) }, shape-detected — any name, not just literal Nat). The transpiler lifts such a type’s VALUES to Lean Nat (Zero→0, Succ x→x + 1), so the dumped goal speaks Nat. Inverting that deterministic lift here — 0→T.Zero, x + 1 / Nat.succ x→T.Succ x, literal n≤8→Succ^n(Zero) — stays inside the translator image (it undoes OUR OWN lift, not a guess). Nat truncated subtraction / mul / div and any non-+1 Nat arithmetic stay OUT of grammar, so the #630 boundary against foreign Nat semantics is untouched. None (no Peano given) = exactly the pre-V2 behavior.

Fields

peano: Option<PeanoCtx>

Trait Implementations

impl Clone for UntranslateCtx

fn clone(&self) -> UntranslateCtx

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UntranslateCtx

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

Formats the value using the given formatter.

impl Default for UntranslateCtx

fn default() -> UntranslateCtx

Returns the “default value” for a type.