law value_eq

bend-osdev-word64@0.1.1.0 · LAWS.bend:77

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

77# Two words with the same value are the same word.
78law value_eq:
79  for +a: W.W64
80  for +b: W.W64
81  for e: {W.W64.to_nat(a) == W.W64.to_nat(b) : Nat}
82  {a == b : W.W64}