Function reify 

pub fn reify(
    term: &Term,
    vars: &mut VarInterner,
) -> Result<Polynomial, ReifyError>

Reify a Syntax term into a polynomial representation.

This function converts the deep embedding of terms (Syntax) into the internal polynomial representation used for normalization.

Supported Term Forms

• SLit n - Integer literal becomes a constant polynomial
• SVar i - De Bruijn variable becomes a polynomial variable
• SName "x" - Named global becomes a polynomial variable (interned)
• SApp (SApp (SName "add") a) b - Addition of two terms
• SApp (SApp (SName "sub") a) b - Subtraction of two terms
• SApp (SApp (SName "mul") a) b - Multiplication of two terms

Errors

Returns ReifyError::NonPolynomial for unsupported operations (div, mod) or unknown function symbols.

Named Variables

Named globals draw their indices from vars, so distinct names get distinct variables and repeated names get the same one. Every term reified for one goal must share one interner — comparing polynomials reified under different interners is meaningless.