law wcmp

lawful-words@0.1.0.0 · proof_word.bend:214

import Base

214# Words compare as their numbers.
215law wcmp:
216  for +n: Nat
217  for +a: Word(n)
218  for +b: Word(n)
219  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}