BendMlLlama.KV: type of bend-ml-llama@0.2.1.0
Import: import bend-ml-llama@0.2.1.0/main.bend as BendMlLlama
Lines 472-477 of bend-ml-llama@0.2.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-llama@0.2.1.0/main.bend&start_line=472&end_line=477

import Base

# One pair of arrays per key/value head: the keys (after RoPE) and the values of positions 0..t-1, position p at
# [p·head, p·head + head). The type indexes are the capacity cap (the positions the arrays have room for, set by
# KV.empty) and t, the number of positions written. KV.push asks for a proof that t < cap, so a cache is never
# written past its room (kv_room says why that is enough).
type KV<-cap: Nat, -t: Nat> is Type:
  KV{ks: List<&1, Array<F32>>, vs: List<&1, Array<F32>>}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat