Function decode_level

crates/ffi/src/lean_env.rs:640–666

(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>)

  list: LeanList<LeanBorrowed<'a>>,
) -> Vec<LeanBorrowed<'a>> {
  list.to_vec()
}

/// Collect list elements as LeanShared handles for cross-thread use.
/// The caller should have already MT-marked the parent list via `LeanShared::new`,
/// so `lean_mark_mt` on each element is a single `lean_is_st` check (fast no-op).
fn collect_list_shared(list: LeanList<LeanBorrowed<'_>>) -> Vec<LeanShared> {
  list.iter().map(|b| LeanShared::new(b.to_owned_ref())).collect()
}

// Name decoding with global cache
pub fn decode_name(obj: LeanBorrowed<'_>, global: &GlobalCache) -> Name {
  let ptr = obj.as_raw();
  // Fast path: check if already cached
  if let Some(name) = global.names.get(&ptr) {
    return name.clone();
  }

  // Compute the name
  let name = if obj.is_scalar() {
    Name::anon()
  } else {
    let n = LeanIxName::from_ctor(obj.as_ctor());
    let pre = decode_name(n.get_obj(0), global);
    let pos = n.get_obj(1);
    match n.as_ctor().tag() {
      1 => Name::str(pre, pos.as_string().to_string()),
      2 => Name::num(pre, LeanNat::to_nat(&pos)),
      tag => unreachable!("Invalid Lean.Name tag: {tag}"),
    }