( syn_ptr: LeanIxSyntax<LeanBorrowed<'_>>, )
| 422 | #[cfg(feature = "test-ffi")] |
| 423 | #[unsafe(no_mangle)] |
| 424 | pub extern "C" fn rs_roundtrip_ix_syntax( |
| 425 | syn_ptr: LeanIxSyntax<LeanBorrowed<'_>>, |
| 426 | ) -> LeanIxSyntax<LeanOwned> { |
| 427 | let syn = syn_ptr.decode(); |
| 428 | let mut cache = LeanBuildCache::new(); |
| 429 | LeanIxSyntax::build(&mut cache, &syn) |
| 430 | } |
| 431 | |
| 432 | /// Round-trip an Ix.DataValue: decode from Lean, re-encode. |
| 433 | #[cfg(feature = "test-ffi")] |