Struct RefinementInfo 

pub struct RefinementInfo<'a> {
    pub carrier_type: &'a str,
    pub carrier_field: &'a str,
    pub param_name: &'a str,
    pub constructor_fn: &'a str,
    pub predicate: &'a Spanned<Expr>,
}

A “refinement record” is the canonical refinement-via-opaque pattern: a single-field record X { carrier: T } paired with a validating smart constructor fn fromX(p: T) -> Result<X, _> body = match <pred-in-p> with true -> Result.Ok(X(carrier = p)) false -> Result.Err("...")

Detecting this shape lets backends emit the type as a true dependent / subset type (def X := { n : T // P n } in Lean, type X = n: T | P n in Dafny) instead of a flat product, which in turn collapses universal-law proofs into one-liners (rw [Int.add_comm]) by carrying the invariant inside the type rather than threading it through ad-hoc tactic plumbing.

Fields

carrier_type: &'a str

Carrier-type annotation as written in the record field ("Int", "Float", …). Backends emit this as the subset’s underlying type.

carrier_field: &'a str

Carrier-field name (e.g. "value"). Lean projects through .val on a Subtype, so users of the carrier field have to rewrite n.value → n.val when the host type is refined.

param_name: &'a str

Name of the smart constructor’s input parameter ("n" in fromInt(n: Int) → Result<X, _>). Used when substituting the law’s quantified variable into the predicate.

constructor_fn: &'a str

Source-level name of the smart constructor itself ("fromInt"). The interval analysis gates its transparent-wrapper peel on this name so only the real smart constructor — never an arbitrary one-arg helper — is treated as identity over its argument.

predicate: &'a Spanned<Expr>

AST node for the bool predicate the smart constructor branches on — the body’s Match { subject = <here>, ... }.

Trait Implementations

impl<'a> Clone for RefinementInfo<'a>

fn clone(&self) -> RefinementInfo<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for RefinementInfo<'a>

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

Formats the value using the given formatter.