ProofShift.SF: def of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_shift.bend as ProofShift Lines 235-237 of lawful-bytes@0.1.1.0/proof_shift.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_shift.bend&start_line=235&end_line=237 import Base # The final view: SV at j = L - k. def SF(+xs: List<&2, U32>, +kk: Nat, +ll: Nat) -> List<&2, U32>: SV(xs, kk, Nat.sub(ll, kk)) Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_shift.bend&name=SV