src/Keys.bend fails

raw source on the hub · import 0x05fa0e42448e8e221df592b204de523d/src/Keys.bend as Keys

1 import

import Base

Definitions

def unpack source · line 6 · raw

@p: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

@+a:String -> @+b:String -> Cmp

def eq source · line 14 · raw

@+a:String -> @+b:String -> Bool

def cmp_is_lt source · line 18 · raw

@c:Cmp -> Bool

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

def cmp_is_eq source · line 21 · raw

@c:Cmp -> Bool

def cmp_is_gt source · line 24 · raw

@c:Cmp -> Bool

def cmp_is_le source · line 27 · raw

@c:Cmp -> Bool

def lt source · line 30 · raw

@+a:String -> @+b:String -> Bool

def le source · line 33 · raw

@+a:String -> @+b:String -> Bool

def cmp_reverse source · line 36 · raw

@c:Cmp -> Cmp

def implies source · line 45 · raw

@a:Bool -> @b:Bool -> Bool

def iff source · line 52 · raw

@+a:Bool -> @+b:Bool -> Bool

def one_hot3 source · line 56 · raw

@a:Bool -> @b:Bool -> @c:Bool -> Bool

True exactly when one of three arbitrary predicates is true.

def cmp_one_hot source · line 68 · raw

@+c:Cmp -> Bool

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

def cmp_one_hot_proof source · line 71 · raw

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

def cmp_eq_pair source · line 82 · raw

@p:Pair(Pair(String, String), Cmp) -> {cmp_is_eq(unpack(p)) == String.eq.fin(p) : 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

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

def bool_refl source · line 101 · raw

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

def word_refl source · line 108 · raw

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

def u32_refl source · line 121 · raw

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

def char_refl source · line 127 · raw

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

def s_cmp_pair_refl source · line 133 · raw

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

def str_refl source · line 142 · raw

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

def str_eq_refl source · line 146 · raw

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