law wlt

lawful-words@0.1.0.0 · proof_word.bend:125

import Base

125# Every word stands for a number below 2^n.
126law wlt:
127  for +n: Nat
128  for +w: Word(n)
129  {Nat.is_lt(Word.to_nat(n, w), Nat.pow(2n, n)) == True{} : Bool}