Function lean_telescope

crates/compile/src/decompile.rs:4675–4684

Extract the source-order `(head, args)` telescope from a Lean App spine. Used by tests to assert the reconstructed spine matches expectations.

(e: &LeanExpr)

  // Insert .below constants via roundtrip_block.
  if needs_below {
    let below_members: Vec<&Name> = aux_members
      .iter()
      .filter(|(k, _)| *k == AuxKind::Below)
      .map(|(_, n)| n)
      .collect();

    let all_below_names: Vec<Name> = below_consts
      .iter()
      .map(|bc| match bc {
        BelowConstant::Indc(i) => i.name.clone(),
        BelowConstant::Def(d) => d.name.clone(),
      })
      .collect();