Function compile_univ

crates/compile/src/compile.rs:379–423

Compile a Lean Level to an Ixon Univ.

(
  level: &Level,
  univ_params: &[Name],
  cache: &mut BlockCache,
)

    if let Some(mut entry) = self.env.named.get_mut(name) {
      entry.value_mut().set_original(orig_addr, orig_meta);
    }
    Ok(())
  }
}

// ===========================================================================
// Helper functions
// ===========================================================================

/// Convert a Nat to u64, returning an error if the value is too large.
fn nat_to_u64(n: &Nat, context: &'static str) -> Result<u64, CompileError> {
  n.to_u64().ok_or(CompileError::UnsupportedExpr { desc: context.into() })
}

// ===========================================================================
// Name compilation
// ===========================================================================

/// Store a string as a blob and return its address.
pub fn store_string(s: &str, stt: &CompileState) -> Address {
  stt.env.store_blob(s.as_bytes().to_vec())
}

/// Store a Nat as a blob and return its address.
pub fn store_nat(n: &Nat, stt: &CompileState) -> Address {
  stt.env.store_blob(n.to_le_bytes())
}

/// Compile a Lean Name to an address (stored in env.names).
/// Uses the Name's internal hash as the address.
/// String components are stored in blobs.
pub fn compile_name(name: &Name, stt: &CompileState) -> Address {
  // Use the Name's internal hash as the address
  let addr = Address::from_blake3_hash(*name.get_hash());

  // Check if already stored
  if stt.env.names.contains_key(&addr) {
    return addr;
  }

  // Recurse on parent first (ensures parent is stored)
  match name.as_data() {
    NameData::Anonymous(_) => {},
    NameData::Str(parent, s, _) => {
      compile_name(parent, stt);
      store_string(s, stt); // string data in blobs
    },
    NameData::Num(parent, _, _) => {