From d241295020cba4145be4a45c9f7e58b20c149cdb Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 10:52:57 +0000 Subject: [PATCH] doc(Computability.WordRAM): add Main results entry for exec_split (#949) --- Complexity/Computability/WordRAM/Multiword/Transfer.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Complexity/Computability/WordRAM/Multiword/Transfer.lean b/Complexity/Computability/WordRAM/Multiword/Transfer.lean index d94efb147f..c8f0feba9b 100644 --- a/Complexity/Computability/WordRAM/Multiword/Transfer.lean +++ b/Complexity/Computability/WordRAM/Multiword/Transfer.lean @@ -29,6 +29,7 @@ little endian in the half-word radix. Registers zero through three are reserved * `Cslib.WordRAM.Multiword.Transfer.exec_copy`: exact copying and register preservation. * `Cslib.WordRAM.Multiword.Transfer.exec_constants`: exact installation of bounded constants. * `Cslib.WordRAM.Multiword.Transfer.exec_assemble`: reconstruction when the scalar fits. +* `Cslib.WordRAM.Multiword.Transfer.exec_split`: exact conversion with sufficient capacity. * `Cslib.WordRAM.Multiword.Transfer.exec_split_eighteen`: exact eighteen-digit conversion. ## References