proofs/containers/hash_table/keys.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as Keys

7 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/u32alg.bend as A
import ../../../spec/containers/hash_table.bend as S
import ../../../src/containers/hash_table.bend as H
import ./strings.bend as STR
import ../../lib/u32.bend as UW

Definitions

def chr_refl source · line 14 · raw

@+c:Char -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.chr_eq(c, c) == True{} : Bool}

def str_refl source · line 19 · raw

@+s:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(s, s) == True{} : Bool}

def chr_eq_of source · line 26 · raw

@+a:Char -> @+b:Char -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.chr_eq(a, b) == True{} : Bool} -> {a == b : Char}

def str_eq_of source · line 32 · raw

@+a:String -> @+b:String -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == True{} : Bool} -> {a == b : String}

equal by str_eq means equal

def str_eq_true source · line 45 · raw

@+a:String -> @+b:String -> @+e:{a == b : String} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == True{} : Bool}

def sym_c source · line 48 · raw

@+a:String -> @+b:String -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == c : Bool} -> @+d:Bool -> @+hd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(b, a) == d : Bool} -> {c == d : Bool}

def str_sym source · line 59 · raw

@+a:String -> @+b:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(a, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.str_eq(b, a) : Bool}

def short_c source · line 65 · raw

@+c:U32 -> @t:String -> Bool

a one-character key whose code is below 2^31 (stored by its word alone)

def shortk source · line 72 · raw

@key:String -> Bool

def kw_c source · line 79 · raw

@+c:U32 -> @+t:String -> @sh:Bool -> U32

def kword source · line 86 · raw

@key:String -> U32

def kword_long source · line 93 · raw

@+key:String -> @+hk:{shortk(key) == False{} : Bool} -> {kword(key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.lword(key) : U32}

def kword_short source · line 100 · raw

@+c:U32 -> @+hc:{U32.is_lt(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.tag) == True{} : Bool} -> {kword(SCon{Chr{c}, ""}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.short_word(c) : U32}

def not_true_eq source · line 103 · raw

@+b:Bool -> @+h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def not_true_eq2 source · line 110 · raw

@+b:Bool -> @+h:{Bool.not(b) == False{} : Bool} -> {b == True{} : Bool}