Function structural_position 

pub fn structural_position(ctx: &Context, body: &Term) -> Option<usize>

The single argument POSITION a reducer needs: the Giménez structural column, or None when the guard admits no column at all and therefore no ι rule applies to this fixpoint.

structural_columns answers with the whole measure because the GUARD needs the whole measure. A reducer needs one number, and asking it for [0] is an index into a vector that is empty exactly when the answer is “there is none” — so the two honest outcomes are spelled as Some/None here rather than left to a caller to remember. (fix f. λx₀ … λxₙ. e) a₀ … aₙ unrolls exactly when a_p is constructor-headed, for p this position.

use logicaffeine_kernel::prelude::StandardLibrary;
use logicaffeine_kernel::termination::structural_position;
use logicaffeine_kernel::{Term, Universe};

let ctx = StandardLibrary::context();
let g = |n: &str| Term::Global(n.into());
let v = |n: &str| Term::Var(n.into());
let app = |f: Term, x: Term| Term::App(Box::new(f), Box::new(x));
let lam = |p: &str, t: Term, b: Term| Term::Lambda { param: p.into(), param_type: Box::new(t), body: Box::new(b) };

// Lean's `Nat.add` recurses on its SECOND argument: λm. λn. match n with 0 ⇒ m | k+1 ⇒ (add m k)+1.
let add = lam("m", g("Nat"), lam("n", g("Nat"), Term::Match {
    discriminant: Box::new(v("n")),
    motive: Box::new(lam("_", g("Nat"), g("Nat"))),
    cases: vec![v("m"), lam("k", g("Nat"), app(g("Succ"), app(app(v("add"), v("m")), v("k"))))],
}));
assert_eq!(structural_position(ctx, &add), Some(1));

// No inductive-typed binder: no column, so no ι rule.
let id = lam("A", Term::Sort(Universe::Type(0)), lam("a", v("A"), v("a")));
assert_eq!(structural_position(ctx, &id), None);

A fixpoint the guard would REFUSE gets None, which is the right answer for a reducer too: an unguarded fixpoint has no ι rule, and unrolling one is how a normaliser diverges.