def wsd.pw

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:79

import Base

79def wsd.pw(n: Nat, k: Nat) -> Word(n):
80  match n:
81    case 0n:
82      WNil{}
83    case 1n+ +p:
84      match k:
85        case 0n:
86          WCon{True{}, Word.zero(p)}
87        case 1n+ +j:
88          WCon{False{}, wsd.pw(p, j)}