Place a field's bits, threading the POSITION and the remaining VALUE instead
of recomputing a power per bit.
The motive is a `pi` over both, because the recursion changes both: each turn
writes the low bit of the value at the current position, then hands the
induction the next position and the value halved. The bits are written in
ascending order into disjoint positions, so the order is not observable --
what changed is that no numeral larger than a byte is ever built.
294def sm86PlaceFieldBitsUnchecked =
295 (lambda unrestricted position : Nat .
296 (lambda unrestricted width : Nat .
297 (lambda unrestricted value : Nat .
298 (lambda unrestricted encoded : Bytes .
299 (app
300 (app
301 (app
302 (nat-eliminate
303 (lambda unrestricted current : Nat .
304 (pi unrestricted currentPosition : Nat .
305 (pi unrestricted currentValue : Nat .
306 (pi unrestricted currentBytes : Bytes . Bytes))))
307 (lambda unrestricted currentPosition : Nat .
308 (lambda unrestricted currentValue : Nat .
309 (lambda unrestricted currentBytes : Bytes . currentBytes)))
310 (lambda unrestricted predecessor : Nat .
311 (lambda unrestricted induction : (pi unrestricted currentPosition : Nat . (pi unrestricted currentValue : Nat . (pi unrestricted currentBytes : Bytes . Bytes))) .
312 (lambda unrestricted currentPosition : Nat .
313 (lambda unrestricted currentValue : Nat .
314 (lambda unrestricted currentBytes : Bytes .
315 (eliminate
316 NaturalDivisionState
317 (lambda unrestricted current : (family NaturalDivisionState) . Bytes)
318 (naturalDivisionState currentValue sm86EncodingNaturalTwo)
319 (branch
320 NaturalDivisionStateValue
321 remainder
322 quotient
323 .
324 (induction
325 (succ currentPosition)
326 quotient
327 (sm86PlaceBitAt currentPosition remainder currentBytes)))))))))
328 width)
329 position)
330 value)
331 encoded)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.