0x5f97f469 fails

0x5f97f469d15c04a181dae0e4e64e1d3d

no description

Anonymous package: import it by hash.

Published

2026-09-24

Size

73,748 bytes, 20 files

License

MIT (LICENSE)
MIT (src/LICENSE)
MIT (src/float/LICENSE)

Declarations

78 laws (29 proved), 156 defs, 14 types

Import

import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.bend as Class
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/bin.bend as Bin
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/f32.bend as MF32
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/format.bend as Format
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/num.bend as Num
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/sf32.bend as Sf32
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.bend as MList
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/machine.bend as Machine
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/nat.bend as MNat
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/queue.bend as Queue
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/sim.bend as Sim
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/sorted.bend as Sorted
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/tree.bend as Tree
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/u32.bend as MU32
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/v2.bend as V2
import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/vec.bend as Vec
import 0x5f97f469d15c04a181dae0e4e64e1d3d/stdlib.bend as Stdlib

Modules

• src/class.bend 15 declarations
• src/float/bin.bend 33 declarations
• src/float/f32.bend 60 declarations, 30 laws
• src/float/format.bend 31 declarations
• src/float/num.bend 10 declarations
• src/float/sf32.bend 22 declarations
• src/list.bend 7 declarations, 3 laws
• src/machine.bend 2 declarations, 1 laws
• src/nat.bend 14 declarations, 9 laws
• src/queue.bend 11 declarations, 3 laws
• src/sim.bend 9 declarations, 3 laws
• src/sorted.bend 16 declarations, 9 laws
• src/tree.bend 8 declarations, 1 laws
• src/u32.bend 20 declarations, 17 laws
• src/v2.bend 7 declarations, 2 laws
• src/vec.bend 5 declarations
• stdlib.bend 0 declarations

Other files

• LICENSE 1,101 bytes
• src/LICENSE 1,101 bytes
• src/float/LICENSE 1,101 bytes

Dependencies

No imports from other hub packages.

Dependents

No package in this build imports it.

Status on bend 2.0.36

Error:
- expected : LE.key(key(F32.min(F32.max(x, lo), hi)), key(hi))
- observed : LE.key(key(Bool.pick(F32, F32.is_lt(F32.max(x, lo), hi), F32.max(x, lo), hi)), key(hi))
Context:
- x  : F32
- lo : F32
- hi : F32
- lh : LE.key(key(lo), key(hi))
- m  : F32
Location: clamp_le_hi
527 |   +m = F32.max(x, lo)
528>|   min_le_r.go(~lt, m, hi, F32.is_lt(m, hi), {==}, le_refl.key(key(hi))(le_key_r(key(lo), key(hi))(lh)))
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
529 |

Error:
- expected : Nat.LE(U32.to_nat(U32.min(a, b)), U32.to_nat(b))
- observed : Nat.LE(U32.to_nat(Bool.pick(U32, Cmp.is_lt(U32.cmp(a, b)), a, b)), U32.to_nat(b))
Context:
- a : U32
- b : U32
Location: min_le_r
143 | def min_le_r(a, b):
144>|   min_le_r.go(a, b, U32.is_lt(a, b), {==})
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
145 |

Error:
- expected : Nat.LE(U32.to_nat(U32.min(a, b)), U32.to_nat(b))
- observed : Nat.LE(U32.to_nat(Bool.pick(U32, Cmp.is_lt(U32.cmp(a, b)), a, b)), U32.to_nat(b))
Context:
- a : U32
- b : U32
Location: min_le_r
143 | def min_le_r(a, b):
144>|   min_le_r.go(a, b, U32.is_lt(a, b), {==})
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
145 |

Error:
- expected : Nat.LE(U32.to_nat(U32.min(a, b)), U32.to_nat(b))
- observed : Nat.LE(U32.to_nat(Bool.pick(U32, Cmp.is_lt(U32.cmp(a, b)), a, b)), U32.to_nat(b))
Context:
- a : U32
- b : U32
Location: min_le_r
143 | def min_le_r(a, b):
144>|   min_le_r.go(a, b, U32.is_lt(a, b), {==})
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
145 |