law u32_le_antisym

bend-osdev-u32@0.1.0.0 · LAWS_order.bend:136

import bend-osdev-u32@0.1.0.0/LAWS_order.bend as LAWSOrder
import Base

136law u32_le_antisym:
137  for +a: U32
138  for +b: U32
139  for h1: {U32.is_le(a, b) == True{} : Bool}
140  for h2: {U32.is_le(b, a) == True{} : Bool}
141  {a == b : U32}

Uses (4)

Used by (0)

No other definition uses this definition.