def word_cmp

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

import Base

124def word_cmp(+n: Nat, +a: Word(n), +b: Word(n)) ->
125  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}:
126  match n:
127    case 0n:
128      {==}
129    case 1n+p:
130      match a b:
131        case WCon{+x, +xs} WCon{+y, +ys}:
132          %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}
133          %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}
134          %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}
135          %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}
136          {==}