def AP.pw

bend-osdev-array@0.1.0.1 · PROOF.bend:328

import Base

328def AP.pw(n: Nat, d: Nat) -> Word(n):
329  match n:
330    case 0n:
331      WNil{}
332    case 1n+q:
333      match d:
334        case 0n:
335          WCon{True{}, Word.zero(q)}
336        case 1n+e:
337          WCon{False{}, AP.pw(q, e)}