Function hash_expr

crates/ixon/src/sharing.rs:333–338

Compute the hash of a single expression. This is useful for testing hash compatibility with Lean.

(expr: &Arc<Expr>)

/// This is useful for testing hash compatibility with Lean.
pub fn hash_expr(expr: &Arc<Expr>) -> blake3::Hash {
  let (_info_map, ptr_to_hash, _) =
    analyze_block(std::slice::from_ref(expr), false);
  let ptr = expr.as_ref() as *const Expr;
  *ptr_to_hash.get(&ptr).expect("Expression not found in ptr_to_hash")
}

/// Topological sort of subterms (leaves first, parents last).
/// CRITICAL: Keys are sorted by hash bytes for deterministic output.
/// This ensures Lean and Rust produce the same topological order.