law u32_eq_of_is_eq

bend-mathlib@0.8.1.0 · string.bend:290

import bend-mathlib@0.8.1.0/string.bend as String
import Base

290# Two U32s that U32.is_eq calls equal are equal.
291law u32_eq_of_is_eq:
292  for a: U32
293  for b: U32
294  for h: {U32.is_eq(a, b) == True{} : Bool}
295  {a == b : U32}

Uses (4)

Used by (2)