def Word.cmp

Base · base.bend:1329

1329def Word.cmp(n: Nat, a: Word(n), b: Word(n)) -> Cmp:
1330  match n:
1331    case 0n:
1332      EQ{}
1333    case 1n+p:
1334      match a b:
1335        case WCon{ab, at} WCon{bb, bt}:
1336          Word.cmp.fin(ab, bb, Word.cmp(p, at, bt))