( constant_obj: LeanIxonConstant<LeanBorrowed<'_>>, bytes_obj: LeanByteArray<LeanBorrowed<'_>>, )
| 55 | |
| 56 | /// Twin parity check for the frozen `mk*` rebuild closure |
| 57 | /// (`reduce_univ` vs `Ixon.reduceUniv`). |
| 58 | #[unsafe(no_mangle)] |
| 59 | pub extern "C" fn rs_reduce_univ_matches( |
| 60 | univ_obj: LeanIxonUniv<LeanBorrowed<'_>>, |
| 61 | expected_obj: LeanIxonUniv<LeanBorrowed<'_>>, |
| 62 | ) -> bool { |
| 63 | let univ = Arc::new(univ_obj.decode()); |
| 64 | let expected = expected_obj.decode(); |
| 65 | *ixon::canon_univ::reduce_univ(&univ) == expected |
| 66 | } |
| 67 | |
| 68 | /// Check if Lean's Ixon.Expr serialization matches Rust. |
| 69 | #[unsafe(no_mangle)] |