package.bend checks
raw source on the hub · import 0x5a02f49892413b8561a33a7642d823e2/package.bend as Package
bend-i64: package entry for BendHub. Source: https://github.com/phenomenon0/bend-i64
SIGNED 64-bit integers, two's complement over Word(64n). add_comm is checked at 64 by instantiating Base's generic lemma Word.add_comm(64n, ...), and it transfers to the signed reading exactly because addition ignores the sign. Signedness lives in: neg (0 - x), cmp (bias both operands by the sign bit), shr.s (arithmetic shift). Pure Bend: no FFI, no intrinsics, no unsafe.
2 imports
import Base import ./i64.bend as I64
Definitions
def zero source · line 12 · raw
0x5a02f49892413b8561a33a7642d823e2/i64.I64
def one source · line 15 · raw
0x5a02f49892413b8561a33a7642d823e2/i64.I64
def minus_one source · line 18 · raw
0x5a02f49892413b8561a33a7642d823e2/i64.I64
def min source · line 21 · raw
0x5a02f49892413b8561a33a7642d823e2/i64.I64
def max source · line 24 · raw
0x5a02f49892413b8561a33a7642d823e2/i64.I64
def add source · line 27 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def sub source · line 30 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def mul source · line 33 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def inc source · line 36 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def neg source · line 39 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def and source · line 42 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def or source · line 45 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def xor source · line 48 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def not source · line 51 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def shl source · line 54 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def shl_n source · line 57 · raw
@n:Nat -> @a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def shr source · line 60 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def shr_s source · line 63 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def shr_s_n source · line 66 · raw
@n:Nat -> @a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> 0x5a02f49892413b8561a33a7642d823e2/i64.I64
def cmp source · line 69 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Cmp
def is_eq source · line 72 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Bool
def is_lt source · line 75 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Bool
def is_gt source · line 78 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> @b:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Bool
def is_neg source · line 81 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Bool
def to_nat source · line 84 · raw
@a:0x5a02f49892413b8561a33a7642d823e2/i64.I64 -> Nat