bend-lawful-stdlib Releases (1): 0.1.0.0 0x5f97f469d15c04a181dae0e4e64e1d3d indexed https://jend.leeeet.dev/files.txt?path=bend-lawful-stdlib@0.1.0.0 Definitions (248, 1 to 100 shown): Class.Ord (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Ord) # a total order: a relation and a decision that returns the side that holds type Ord<-A: Data> is Type: Ord{R: A -> A -> Type, dec: @x: A -> @y: A -> Or(R(x, y), R(y, x))} Class.Ord.R (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Ord.R) def Ord.R(-A: Data, d: Ord, x: A, y: A) -> Type: Class.Ord.dec (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Ord.dec) def Ord.dec(-A: Data, d: Ord, x: A, y: A) -> Or(Ord.R(A, d, x, y), Ord.R(A, d, y, x)): Class.Semigroup (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup) # an associative operation type Semigroup<-A: Data> is Type: Semigroup{op: A -> A -> A, assoc: @x: A -> @y: A -> @z: A -> {op(x, op(y, z)) == op(op(x, y), z) : A}} Class.Semigroup.op (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.op) def Semigroup.op(-A: Data, d: Semigroup, x: A, y: A) -> A: Class.Semigroup.fn (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.fn) # op as a template function, for Base's templates (List.foldr, List.foldl) def Semigroup.fn(~A: Data, ~d: Semigroup, x: A, y: A) -> A: Class.Semigroup.assoc (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.assoc) def Semigroup.assoc(-A: Data, d: Semigroup, x: A, y: A, z: A) -> {Semigroup.op(A, d, x, Semigroup.op(A, d, y, z)) == Semigroup.op(A, d, Semigroup.op(A, d, x, y), z) : A}: Class.Group (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Group) # addition and subtraction that undo each other (wrapping integers) type Group<-A: Data> is Type: Group{add: A -> A -> A, sub: A -> A -> A, sub_add: @a: A -> @b: A -> {a == sub(add(a, b), b) : A}, add_sub: @a: A -> @b: A -> {a == add(sub(a, b), b) : A}} Class.Group.add (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Group.add) def Group.add(-A: Data, d: Group, a: A, b: A) -> A: Class.Group.sub (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Group.sub) def Group.sub(-A: Data, d: Group, a: A, b: A) -> A: Class.Group.sub_add (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Group.sub_add) def Group.sub_add(-A: Data, d: Group, a: A, b: A) -> {a == Group.sub(A, d, Group.add(A, d, a, b), b) : A}: Class.Group.add_sub (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Group.add_sub) def Group.add_sub(-A: Data, d: Group, a: A, b: A) -> {a == Group.add(A, d, Group.sub(A, d, a, b), b) : A}: Bin.Bin (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=Bin) type Bin is Data: BZ{} B0{r: Bin} B1{r: Bin} Bin.one (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=one) def one() -> Bin: Bin.is_zero (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=is_zero) def is_zero(a: Bin) -> Bool: Bin.trim.cons0 (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=trim.cons0) def trim.cons0(t: Bin) -> Bin: Bin.trim (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=trim) # the same number without high zero bits, so equal numbers are equal terms def trim(a: Bin) -> Bin: Bin.odd (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=odd) def odd(a: Bin) -> Bool: Bin.inc (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=inc) def inc(a: Bin) -> Bin: Bin.cons (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=cons) def cons(s: Bool, r: Bin) -> Bin: Bin.adc.one (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=adc.one) def adc.one(a: Bin, c: Bool) -> Bin: Bin.adc (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=adc) # a + b + carry, one bit at a time: bits 0+0 pass the carry through and # carry nothing, 0+1 flip it and carry it, 1+1 pass it and carry one def adc(a: Bin, b: Bin, +c: Bool) -> Bin: Bin.add (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=add) def add(a: Bin, b: Bin) -> Bin: Bin.dec (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=dec) def dec(a: Bin) -> Bin: Bin.sbb.one (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=sbb.one) def sbb.one(a: Bin, w: Bool) -> Bin: Bin.sbb (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=sbb) # a - b - borrow, for a >= b (callers order the operands with cmp first) def sbb(a: Bin, b: Bin, +w: Bool) -> Bin: Bin.sub (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=sub) def sub(a: Bin, b: Bin) -> Bin: Bin.mul (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=mul) def mul(a: Bin, +b: Bin) -> Bin: Bin.cmp.fin (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=cmp.fin) def cmp.fin(p: Bool, q: Bool, hi: Cmp) -> Cmp: Bin.cmp (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=cmp) def cmp(a: Bin, b: Bin) -> Cmp: Bin.shl (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=shl) # a * 2^n def shl(a: Bin, n: Nat) -> Bin: Bin.pow2 (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=pow2) def pow2(n: Nat) -> Bin: Bin.len.up (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=len.up) def len.up(l: Nat) -> Nat: Bin.len (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=len) # number of significant bits def len(a: Bin) -> Nat: Bin.shr (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=shr) # a / 2^k, with the last bit shifted out (round) and whether any bit # below it was set (sticky); r and s are the bits already shifted out def shr(k: Nat, a: Bin, r: Bool, s: Bool) -> Bin & Bool & Bool: Bin.of_word (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=of_word) # the n low bits of a word, and back def of_word(n: Nat, w: Word(n)) -> Bin: Bin.to_word (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=to_word) def to_word(n: Nat, a: Bin) -> Word(n): Bin.to_nat (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=to_nat) def to_nat(a: Bin) -> Nat: Bin.of_nat (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=of_nat) def of_nat(n: Nat) -> Bin: Bin.low (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=low) # the low k bits of a def low(k: Nat, a: Bin) -> Bin: Bin.take.cons (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=take.cons) def take.cons(-r: Nat, b: Bool, p: Bin & Word(r)) -> Bin & Word(r): Bin.take (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/bin.bend&name=take) # the low k bits of a word as a Bin, and the word that remains def take(k: Nat, -r: Nat, w: Word(Nat.add(k, r))) -> Bin & Word(r): F32.void (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=void) def void(-A: Type, v: Empty) -> A: F32.no_f (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=no_f) # {False == True} and {True == False} are empty def no_f(e: {False{} == True{} : Bool}) -> Empty: F32.no_t (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=no_t) def no_t(e: {True{} == False{} : Bool}) -> Empty: F32.first (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=first) def first(r: Word(31n) & Bool) -> Word(31n): F32.split.cons (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=split.cons) def split.cons(-n: Nat, b: Bool, r: Word(n) & Bool) -> Word(1n+n) & Bool: F32.split (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=split) # a word's first n bits, and its last bit (the sign, for n = 31) def split(n: Nat, w: Word(1n+n)) -> Word(n) & Bool: F32.unsplit (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=unsplit) # a word with s appended as its last bit def unsplit(n: Nat, w: Word(n), s: Bool) -> Word(1n+n): F32.split_unsplit (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=split_unsplit) law split_unsplit: for n: Nat for w: Word(n) for s: Bool {(w, s) == split(n, unsplit(n, w, s)) : Word(n) & Bool} F32.mag (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=mag) # the 31 bits below the sign: exponent and fraction def mag(x: F32) -> Word(31n): F32.neg.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg.go) def neg.go(r: Word(31n) & Bool) -> Word(32n): F32.neg_bits (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_bits) # IEEE 754 negation: the sign bit flipped def neg_bits(x: F32) -> F32: F32.Key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=Key) # how the IEEE order reads a float: NaN, or a number with a sign and a # magnitude. # Magnitudes are ordered as integers; above infinity's they are NaNs. type Key is Data: KNaN{} Num{neg: Bool, mag: Word(31n)} F32.IsKey (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=IsKey) def IsKey(k: Key) -> Data: F32.inf_mag.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=inf_mag.go) # infinity's magnitude, 0x7F800000 def inf_mag.go(x: U32) -> F32: F32.inf_mag (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=inf_mag) def inf_mag() -> F32: F32.key.cls (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=key.cls) def key.cls(s: Bool, m: Word(31n), c: Cmp) -> Key: F32.key.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=key.go) def key.go(r: Word(31n) & Bool) -> Key: F32.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=key) def key(x: F32) -> Key: F32.zero (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=zero) def zero(m: Word(31n)) -> Bool: F32.lt.signs (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt.signs) def lt.signs(s: Bool, t: Bool, +x: Word(31n), +y: Word(31n)) -> Bool: F32.lt.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt.key) def lt.key(a: Key, b: Key) -> Bool: F32.lt_bits (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt_bits) # IEEE 754 a < b: false when either is NaN; -0 and +0 are equal def lt_bits(a: F32, b: F32) -> Bool: F32.NotGT (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=NotGT) def NotGT(c: Cmp) -> Data: F32.le.signs (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=le.signs) def le.signs(s: Bool, t: Bool, +x: Word(31n), +y: Word(31n)) -> Type: F32.LE.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=LE.key) def LE.key(a: Key, b: Key) -> Type: F32.LE (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=LE) # a <= b in the IEEE order, as a type: Empty when either is NaN def LE(a: F32, b: F32) -> Type: F32.swap (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=swap) def swap(c: Cmp) -> Cmp: F32.bool_cmp_refl (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=bool_cmp_refl) law bool_cmp_refl: for x: Bool {EQ{} == Bool.cmp(x, x) : Cmp} F32.Word.cmp_refl (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=Word.cmp_refl) law Word.cmp_refl: for +n: Nat for a: Word(n) {EQ{} == Word.cmp(n, a, a) : Cmp} F32.fin_swap (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=fin_swap) law fin_swap: for c: Cmp for x: Bool for y: Bool {swap(Word.cmp.fin(x, y, c)) == Word.cmp.fin(y, x, swap(c)) : Cmp} F32.Word.cmp_swap (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=Word.cmp_swap) law Word.cmp_swap: for +n: Nat for a: Word(n) for b: Word(n) {swap(Word.cmp(n, a, b)) == Word.cmp(n, b, a) : Cmp} F32.lt_notgt (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt_notgt) law lt_notgt: for c: Cmp {Cmp.is_lt(c) == True{} : Bool} -> NotGT(c) F32.notlt_swap (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=notlt_swap) law notlt_swap: for c: Cmp {Cmp.is_lt(c) == False{} : Bool} -> NotGT(swap(c)) F32.lt_le.signs (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt_le.signs) law lt_le.signs: for s: Bool for t: Bool for +x: Word(31n) for +y: Word(31n) {lt.signs(s, t, x, y) == True{} : Bool} -> le.signs(s, t, x, y) F32.lt_le.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt_le.key) # a < b gives a <= b law lt_le.key: for a: Key for b: Key {lt.key(a, b) == True{} : Bool} -> LE.key(a, b) F32.lt_key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lt_key) # only an ordered value is below something law lt_key: for a: Key for b: Key {lt.key(a, b) == True{} : Bool} -> IsKey(a) F32.le_key_l (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=le_key_l) law le_key_l: for a: Key for b: Key LE.key(a, b) -> IsKey(a) F32.le_key_r (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=le_key_r) law le_key_r: for a: Key for b: Key LE.key(a, b) -> IsKey(b) F32.le_refl.signs (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=le_refl.signs) law le_refl.signs: for s: Bool for +m: Word(31n) le.signs(s, s, m, m) F32.le_refl.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=le_refl.key) law le_refl.key: for k: Key IsKey(k) -> LE.key(k, k) F32.total.same (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=total.same) law total.same: for +x: Word(31n) for +y: Word(31n) for e: {Cmp.is_lt(Word.cmp(31n, x, y)) == False{} : Bool} NotGT(Word.cmp(31n, y, x)) F32.total.mixed (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=total.mixed) law total.mixed: for +x: Word(31n) for +y: Word(31n) for e: {lt.signs(True{}, False{}, x, y) == False{} : Bool} Nat.IsFalse(lt.signs(True{}, False{}, x, y)) F32.total.signs (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=total.signs) law total.signs: for s: Bool for t: Bool for +x: Word(31n) for +y: Word(31n) {lt.signs(s, t, x, y) == False{} : Bool} -> le.signs(t, s, y, x) F32.total.key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=total.key) # two ordered values: not a < b gives b <= a law total.key: for a: Key for b: Key IsKey(a) -> IsKey(b) -> {lt.key(a, b) == False{} : Bool} -> LE.key(b, a) F32.LtOk (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=LtOk) # the hardware's < is IEEE 754's def LtOk() -> Type: F32.NegOk (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=NegOk) # the hardware's negation flips the sign bit of every non-NaN float. A # NaN's sign and payload are left out: the JS lane does not keep them. def NegOk() -> Type: F32.bits_lt (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=bits_lt) law bits_lt: for ~lt: LtOk() for +a: F32 for +b: F32 for -c: Bool for e: {F32.is_lt(a, b) == c : Bool} {lt_bits(a, b) == c : Bool} F32.min_le_r.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=min_le_r.go) law min_le_r.go: for ~lt: LtOk() for +a: F32 for +b: F32 for c: Bool for e: {F32.is_lt(a, b) == c : Bool} for bb: LE(b, b) LE(Bool.pick(F32, c, a, b), b) F32.clamp_le_hi (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=clamp_le_hi) # clamp(x, lo, hi) <= hi for every x, NaN and infinities included law clamp_le_hi: for ~lt: LtOk() for +x: F32 for +lo: F32 for +hi: F32 for lh: LE(lo, hi) LE(F32.clamp(x, lo, hi), hi) F32.lo_le_clamp.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lo_le_clamp.go) law lo_le_clamp.go: for ~lt: LtOk() for +x: F32 for +lo: F32 for +hi: F32 for c1: Bool for e1: {F32.is_lt(x, lo) == c1 : Bool} for c2: Bool for e2: {F32.is_lt(Bool.pick(F32, c1, lo, x), hi) == c2 : Bool} for lh: LE(lo, hi) LE(lo, Bool.pick(F32, c2, Bool.pick(F32, c1, lo, x), hi)) F32.lo_le_clamp (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=lo_le_clamp) # lo <= clamp(x, lo, hi) for every x, when lo <= hi law lo_le_clamp: for ~lt: LtOk() for +x: F32 for +lo: F32 for +hi: F32 for lh: LE(lo, hi) LE(lo, F32.clamp(x, lo, hi)) F32.neg_mag.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_mag.go) law neg_mag.go: for r: Word(31n) & Bool {first(r) == first(split(31n, neg.go(r))) : Word(31n)} F32.neg_mag.bits (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_mag.bits) law neg_mag.bits: for a: F32 {mag(a) == mag(neg_bits(a)) : Word(31n)} F32.neg_mag (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_mag) # |-a| is |a|, bit for bit law neg_mag: for ~ng: NegOk() for +a: F32 for ka: IsKey(key(a)) {mag(a) == mag(F32.neg(a)) : Word(31n)} F32.key_sign (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=key_sign) # whether a value is NaN does not depend on its sign law key_sign: for s: Bool for t: Bool for m: Word(31n) for c: Cmp IsKey(key.cls(s, m, c)) -> IsKey(key.cls(t, m, c)) F32.neg_key.go (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_key.go) law neg_key.go: for r: Word(31n) & Bool IsKey(key.go(r)) -> IsKey(key.go(split(31n, neg.go(r)))) F32.neg_key.bits (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_key.bits) law neg_key.bits: for a: F32 IsKey(key(a)) -> IsKey(key(neg_bits(a))) F32.neg_key (https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/float/f32.bend&name=neg_key) # the negation of a non-NaN is not NaN law neg_key: for ~ng: NegOk() for +a: F32 for +ka: IsKey(key(a)) IsKey(key(F32.neg(a))) More: https://jend.leeeet.dev/packages/bend-lawful-stdlib.txt?definitions_offset=100