Route.cap_word: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/storage/route.bend as Route Lines 269-270 of bendtorch-core@0.1.0.0/src/storage/route.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&start_line=269&end_line=270 import Base import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/size.bend as Size def cap_word(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {U32.to_nat(Size.capacity(d)) == Model.capacity(d) : Nat}: Equal.sym(Nat, Model.capacity(d), U32.to_nat(Size.capacity(d)), cap_nat(d, h)) Uses (8): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=cap_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/size.bend&name=capacity