Struct RefinedTypeDecl 

pub struct RefinedTypeDecl {
    pub name: String,
    pub carrier_type: String,
    pub carrier_field: String,
    pub predicate_param: String,
    pub invariant: Predicate,
    pub witness: Option<String>,
}

A refinement-lifted user type — opaque record with a single carrier field, paired with a validating smart constructor. The presence of this decl in ProofIR.refined_types is the decision: “emit this as a subtype on Lean and a subset type on Dafny”. Backends never re-decide.

Fields

name: String

Source-level type name (e.g. "Natural"). NOT canonicalised — backends emit using the source name; canonical form is the map key.

carrier_type: String

Carrier annotation from the record’s single field (typically "Int"). Drives the Lean Subtype underlying type and the Dafny subset type’s base.

carrier_field: String

Carrier-field source name (e.g. "value"). Lean uses .val to project Subtype values regardless of source name; Dafny’s subset binds the source name in its predicate.

predicate_param: String

Smart constructor’s input parameter name (e.g. "n") — the invariant predicate’s free variable.

invariant: Predicate

Bool predicate that every value of the refined type must satisfy, in terms of predicate_param. Comes from the smart constructor’s match <pred> { true -> Ok(...); false -> Err(...) } subject.

witness: Option<String>

Inhabitation witness: a literal value of carrier_type that the lowerer verified satisfies invariant. Resolved by first trying the smart constructor’s verify block (fromX(K) => Ok(...) for some literal K — verified by the user via aver verify), then evaluating the predicate against small candidates as a fallback.

Why the IR carries this even though only Dafny’s subset type strictly requires a non-emptiness witness: it’s a fact about the type (∃ v : carrier, invariant(v) holds), not a Dafny-specific syntactic obligation. Backends use it as they see fit:

• Dafny: emits type X = v: int | P v witness <W>. Required for the subset type to be inhabited and elaborable.
• Lean: currently unused — propositional Subtype may be empty, so { v : Int // P v } elaborates regardless. Step N+1 could emit a def sample_X : X := ⟨W, by decide⟩ for roundtrip / test convenience.
• Future Z3 / Coq / etc.: same fact, rendered per target.

None when no satisfier was found. Backends that require a witness must either reject the type or fall back to a target- default (Dafny picks 0 and crosses fingers).

Trait Implementations

impl Clone for RefinedTypeDecl

fn clone(&self) -> RefinedTypeDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RefinedTypeDecl

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

Formats the value using the given formatter.