ProofGen.ncnt: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen Lines 906-912 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=906&end_line=912 import Base # How many elements of xs are within one step of a. def ncnt(+a: Nat, xs: List<&2, Nat>) -> Nat: match xs: case Nil{}: 0n case x <> t: Nat.add(one(nr(a, x)), ncnt(a, t)) 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.add https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=nr https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=one