Loop.last2: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop Lines 33-36 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&start_line=33&end_line=36 import Base import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T def last2(rest: List<&2,T.Out>, +x: T.Out) -> T.Out: match rest: case Nil{}: x case Con{y,r}: last2(r,y) Uses (2): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out