pub fn enumerate_scopings<'a>(
expr: &'a LogicExpr<'a>,
interner: &mut Interner,
expr_arena: &'a Arena<LogicExpr<'a>>,
_term_arena: &'a Arena<Term<'a>>,
) -> ScopeIterator<'a> ⓘExpand description
Generates all possible quantifier scopings for an expression.
Returns an iterator over all scope-permuted versions of the expression,
respecting scope island constraints. Quantifiers with the same island_id
can be permuted; quantifiers in different islands maintain relative order.
§Example
“Every man loves a woman” has two readings:
- Surface scope: ∀x(Man(x) → ∃y(Woman(y) ∧ Love(x,y)))
- Inverse scope: ∃y(Woman(y) ∧ ∀x(Man(x) → Love(x,y)))