CoreModel.get: def of bend-collections@1.0.0.0 Import: import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as CoreModel Lines 9-16 of bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend&start_line=9&end_line=16 import Base def get(xs: List<&2, U32>, n: Nat) -> U32: match xs n: case Nil{} _: 0 case h <> t 0n: h case h <> t 1n+p: get(t, p) Uses (3): 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=U32