ProofFastFind.hd_eq: def of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_find.bend as ProofFastFind Lines 143-149 of lawful-bytes@0.1.1.0/proof_fast_find.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&start_line=143&end_line=149 import Base # Whether the head of a list is c. def hd_eq(xs: List<&2, U32>, +c: U32) -> Bool: match xs: case Nil{}: False{} case Con{x, t}: U32.is_eq(x, c) Uses (4): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq