~/bend-docscommunity

proofs/lib/lemmas/src/entry_ops.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/entry_ops.bend as Entry_ops

4 imports
import Base
import ../types/model.bend as T
import ./cache.bend as C
import ./time.bend as Time

Definitions

def finish_miss source · line 10 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>

def keys_of source · line 14 · raw

@-K:Data -> @-V:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, K>

def values_of source · line 21 · raw

@-K:Data -> @-V:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, V>

def refresh_prepare_found source · line 28 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def refresh_prepare source · line 35 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def refresh_at source · line 38 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>