src/Keys.bend fails

raw source on the hub · import mylsm-lsm-store@0.3.1.0/src/Keys.bend as Keys

1 import

import Base

Definitions

def unpack source · line 6 · raw

@pair:Pair(Pair(String, String), Cmp) -> Cmp

Total-order comparison for keys. Base's String.cmp hands the strings back beside the verdict ((s1, s2), c); we take reusable copies and unpack via a helper (a match cannot scrutinize the computed call directly).

def cmp source · line 11 · raw

@+s1:String -> @+s2:String -> Cmp

def eq source · line 14 · raw

@+s1:String -> @+s2:String -> Bool

def cmp_is_lt source · line 18 · raw

@ord:Cmp -> Bool

Small, coherent views of Cmp used by key-order laws and sorted-run code.

def cmp_is_eq source · line 21 · raw

@ord:Cmp -> Bool

def cmp_is_gt source · line 24 · raw

@ord:Cmp -> Bool

def cmp_is_le source · line 27 · raw

@ord:Cmp -> Bool

def lt source · line 30 · raw

@+s1:String -> @+s2:String -> Bool

def le source · line 33 · raw

@+s1:String -> @+s2:String -> Bool

def cmp_reverse source · line 36 · raw

@ord:Cmp -> Cmp

def implies source · line 45 · raw

@s1:Bool -> @s2:Bool -> Bool

def iff source · line 52 · raw

@+s1:Bool -> @+s2:Bool -> Bool

def one_hot3 source · line 56 · raw

@first:Bool -> @second:Bool -> @third:Bool -> Bool

True exactly when one of three arbitrary predicates is true.

def cmp_one_hot source · line 68 · raw

@+ord:Cmp -> Bool

Cmp is intrinsically one-hot; this predicate gives K6 a reusable statement.

def cmp_one_hot_proof source · line 71 · raw

@+ord:Cmp -> {cmp_one_hot(ord) == True{} : Bool}

def cmp_eq_pair source · line 82 · raw

@pair:Pair(Pair(String, String), Cmp) -> {cmp_is_eq(unpack(pair)) == String.eq.fin(pair) : Bool}

String.eq is defined by the EQ projection of String.cmp; matching the handed-back comparison pair exposes that definitional correspondence.

def cmp_eq_bridge source · line 93 · raw

@+s1:String -> @+s2:String -> {cmp_is_eq(cmp(s1, s2)) == eq(s1, s2) : Bool}

def bool_refl source · line 101 · raw

@+flag:Bool -> {Bool.cmp(flag, flag) == EQ{} : Cmp}

def word_refl source · line 108 · raw

@width:Nat -> @+word:Word(width) -> {Word.cmp(width, word, word) == EQ{} : Cmp}

def u32_refl source · line 121 · raw

@+val:U32 -> {U32.cmp(val, val) == EQ{} : Cmp}

def char_refl source · line 127 · raw

@+ch:Char -> {Char.cmp(ch, ch) == ((ch, ch), EQ{}) : Pair(Pair(Char, Char), Cmp)}

def s_cmp_pair_refl source · line 133 · raw

@+str:String -> {String.cmp(str, str) == ((str, str), EQ{}) : Pair(Pair(String, String), Cmp)}

def str_refl source · line 142 · raw

@+str:String -> {cmp(str, str) == EQ{} : Cmp}

def str_eq_refl source · line 146 · raw

@+str:String -> {eq(str, str) == True{} : Bool}