( sp_ptr: LeanIxSyntaxPreresolved<LeanBorrowed<'_>>, )
| 411 | #[cfg(feature = "test-ffi")] |
| 412 | #[unsafe(no_mangle)] |
| 413 | pub extern "C" fn rs_roundtrip_ix_syntax_preresolved( |
| 414 | sp_ptr: LeanIxSyntaxPreresolved<LeanBorrowed<'_>>, |
| 415 | ) -> LeanIxSyntaxPreresolved<LeanOwned> { |
| 416 | let sp = sp_ptr.decode(); |
| 417 | let mut cache = LeanBuildCache::new(); |
| 418 | LeanIxSyntaxPreresolved::build(&mut cache, &sp) |
| 419 | } |
| 420 | |
| 421 | /// Round-trip an Ix.Syntax: decode from Lean, re-encode. |
| 422 | #[cfg(feature = "test-ffi")] |