Cache.first_entry: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend as Cache
Lines 265-270 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend&start_line=265&end_line=270

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/types/model.bend as T

def first_entry(-K: Data, -V: Data, c: Cache<K, V>, order: List<&2, String>) -> Maybe<&2, T.Entry<K, V>>:
  match order:
    case Nil{}:
      None{}
    case Con{k, rest}:
      lookup(K, V, c, k)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend&name=Cache
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/cache.bend&name=lookup
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/types/model.bend&name=Entry