Enum ResolvedTopLevel 

pub enum ResolvedTopLevel {
    Module(Module),
    FnDef(ResolvedFnDef),
    Passthrough(TopLevel),
}

Resolved top-level item — mirror of crate::ast::TopLevel. Verify, Decision, TypeDef items pass through with their original AST representation: they aren’t on the runtime hot path, and their internal expressions get resolved lazily by proof-export passes that already consume Expr. Future PRs may promote them.

Variants

Module(Module)

FnDef(ResolvedFnDef)

Passthrough(TopLevel)

Verify / Decision / TypeDef items: passthrough for now. Each carries its original AST node — the resolver lifts only what runtime backends consume. See module doc for the rationale + the future PR that promotes these.

Trait Implementations

impl Clone for ResolvedTopLevel

fn clone(&self) -> ResolvedTopLevel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolvedTopLevel

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

Formats the value using the given formatter.

impl PartialEq for ResolvedTopLevel

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