def wof

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:334

import Base

334# The first n coefficients of a list, zero-filled.
335def wof(n: Nat, bs: List<&2, Bool>) -> Word(n):
336  match n bs:
337    case 0n _:
338      WNil{}
339    case 1n+p Nil{}:
340      WCon{False{}, wof(p, Nil{})}
341    case 1n+p b <> rest:
342      WCon{b, wof(p, rest)}