Function decode_substring

crates/ffi/src/lean_env.rs:668–674

(obj: LeanBorrowed<'_>)

      1 => Name::str(pre, pos.as_string().to_string()),
      2 => Name::num(pre, LeanNat::to_nat(&pos)),
      tag => unreachable!("Invalid Lean.Name tag: {tag}"),
    }
  };

  // Insert and return (entry API handles races gracefully)
  global.names.entry(ptr).or_insert(name).clone()
}

/// Decode an `@& Array Lean.Name` FFI argument into a `Vec<Name>`.
///