def unit

bendtorch-core@0.1.0.0 · src/storage/arith.bend:387

import Base

387def unit(m: Nat, +k: Nat) -> Word(m):
388  match m:
389    case 0n:
390      WNil{}
391    case 1n+q:
392      match k:
393        case 0n:
394          WCon{True{}, Word.zero(q)}
395        case 1n+r:
396          WCon{False{}, unit(q, r)}