BendMlLlama.step_room: def of bend-ml-llama@0.2.1.0
Import: import bend-ml-llama@0.2.1.0/main.bend as BendMlLlama
Lines 573-578 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=573&end_line=578

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

# For callers that walk the positions with a counter of steps left (fuel), keeping t + fuel = cap: with 1 + p steps
# left, position t is below the capacity (step_room), and after the step t + 1 + p = cap still holds (step_inv).
def step_room(+t: Nat, +p: Nat, -cap: Nat, e: {Nat.add(t, 1n+p) == cap : Nat}) -> {True{} == TA.leb(1n+t, cap) : Bool}:
  %e : {True{} == TA.leb(1n+t, _) : Bool}
  %add_succ(t, p) : {True{} == TA.leb(1n+t, _) : Bool}
  TA.leb_up(t, t, p, TA.leb_refl(t))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-ml-llama@0.2.1.0/main.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_refl
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=leb_up