package.bend checks
raw source on the hub · import 0x0f1da4e80677f1d50e6f638a7d6f27ef/package.bend as Package
bend-u64: package entry for BendHub. Source: https://github.com/phenomenon0/bend-u64
64-bit unsigned integers as one Word(64n), with U64.add_comm checked at 64 by instantiating Base's own generic inductive lemma Word.add_comm(64n, ...). Pure Bend: no FFI, no intrinsics, no unsafe, no compiler change. Boundaries: to_nat holds while <= 2^48-1; shl.n/shr.n are O(n) folds.
2 imports
import Base import ./u64.bend as U64
Definitions
def zero source · line 11 · raw
0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def one source · line 14 · raw
0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def max source · line 17 · raw
0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def add source · line 20 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def sub source · line 23 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def mul source · line 26 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def inc source · line 29 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def and source · line 32 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def or source · line 35 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def xor source · line 38 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def not source · line 41 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def shl source · line 44 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def shr source · line 47 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def shl_n source · line 50 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @n:Nat -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def shr_n source · line 53 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @n:Nat -> 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64
def cmp source · line 56 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> Cmp
def is_eq source · line 59 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> Bool
def is_lt source · line 62 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> Bool
def is_gt source · line 65 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> @b:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> Bool
def to_nat source · line 68 · raw
@a:0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.U64 -> Nat