Struct Predicate 

pub struct Predicate {
    pub free_vars: Vec<(String, QuantifierType)>,
    pub expr: Spanned<ResolvedExpr>,
}

A bool predicate with explicit free-variable context. Stays in Spanned<Expr> form so backends can route through their existing emit_expr paths; the context is what gives backends the information they need to project (e.g. .val) without re-walking the AST.

Fields

free_vars: Vec<(String, QuantifierType)>

Variables the predicate may reference, in declaration order. Each entry tells the backend what type the var has in the target language — same logic as Quantifier.binder_type.

expr: Spanned<ResolvedExpr>

The expression. Already in the target variable space (e.g. caller-derived predicates have had caller-arg names substituted to callee-param names).

Trait Implementations

impl Clone for Predicate

fn clone(&self) -> Predicate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Predicate

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

Formats the value using the given formatter.