law fits64

lawful-fields@0.1.1.0 · proof_digits.bend:386

import Base

386# Below 64 is below 2^32 (2^32 only meets itself: pow_lt is symbolic).
387law fits64:
388  for +x: Nat
389  for +hx: {Nat.is_le(x, Nat.pow(2n, 6n)) == True{} : Bool}
390  {Nat.is_lt(x, Nat.pow(2n, 32n)) == True{} : Bool}