Arith.word_cmp: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
Lines 124-136 of bendtorch-core@0.1.0.0/src/storage/arith.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&start_line=124&end_line=136

import Base

def word_cmp(+n: Nat, +a: Word(n), +b: Word(n)) ->
  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}:
  match n:
    case 0n:
      {==}
    case 1n+p:
      match a b:
        case WCon{+x, +xs} WCon{+y, +ys}:
          %word_bit(p, x, xs) : {Nat.cmp(_, Word.to_nat(1n+p, WCon{y, ys})) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
          %word_bit(p, y, ys) : {Nat.cmp(bit(x, Word.to_nat(p, xs)), _) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
          %cmp_bits(Word.to_nat(p, xs), Word.to_nat(p, ys), x, y) : {_ == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
          %word_cmp(p, xs, ys) : {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, xs), Word.to_nat(p, ys))) == Word.cmp.fin(x, y, _) : Cmp}
          {==}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=cmp_bits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=word_bit