Enum QuantifierType 

pub enum QuantifierType {
    Plain(String),
    RefinedTo {
        refined_type: String,
    },
    OracleSubtype(String),
}

Variants

Plain(String)

Plain Aver type, rendered as-is on each backend.

RefinedTo

Refinement-lifted: source declared given a: Int, body used Natural(value = a), so the quantifier binds at the refined type. The carried refined_type key looks up in ProofIR.refined_types.

Fields

refined_type: String

OracleSubtype(String)

Oracle subtype: classified Generative-shape effect-givens bind oracles wrapped in a subtype carrier (RandomIntInBounds, RandomFloatInUnit, TimeUnixMsNonneg).

Trait Implementations

impl Clone for QuantifierType

fn clone(&self) -> QuantifierType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for QuantifierType

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

Formats the value using the given formatter.