U64.LeSigned.value: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/math/u64.bend as U64
Lines 35-36 of bend-collections-laws-math@1.0.0.0/spec/math/u64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/u64.bend&start_line=35&end_line=36

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U

def LeSigned.value(+a: U.U64, +b: U.U64) -> Type:
  {U.le_signed(a, b) == N.order(bits(a), bits(b), N.negative(bits(a)), N.negative(bits(b))) : Bool}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend&name=negative
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend&name=order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/u64.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=le_signed