def AP.lm

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

import Base

339def AP.lm(n: Nat, d: Nat) -> Word(n):
340  match n:
341    case 0n:
342      WNil{}
343    case 1n+q:
344      match d:
345        case 0n:
346          WCon{False{}, Word.zero(q)}
347        case 1n+e:
348          WCon{True{}, AP.lm(q, e)}