| 42 | /// P5 mirror-parity check (canonicity §10.6): does Rust's `canon_univ` |
| 43 | /// of `univ` equal Lean's `Ixon.canonUniv` result `expected` |
| 44 | /// structurally? Byte equality follows from structural equality |
| 45 | /// (`put_univ` is a function of the tree). |
| 46 | #[unsafe(no_mangle)] |
| 47 | pub extern "C" fn rs_canon_univ_matches( |
| 48 | univ_obj: LeanIxonUniv<LeanBorrowed<'_>>, |
| 49 | expected_obj: LeanIxonUniv<LeanBorrowed<'_>>, |
| 50 | ) -> bool { |
| 51 | let univ = Arc::new(univ_obj.decode()); |
| 52 | let expected = expected_obj.decode(); |
| 53 | *ixon::canon_univ::canon_univ(&univ) == expected |
| 54 | } |
| 55 | |
| 56 | /// Twin parity check for the frozen `mk*` rebuild closure |