def ncnt

minebender-game@1.0.0.0 · proof_gen.bend:906

import Base

906# How many elements of xs are within one step of a.
907def ncnt(+a: Nat, xs: List<&2, Nat>) -> Nat:
908  match xs:
909    case Nil{}:
910      0n
911    case x <> t:
912      Nat.add(one(nr(a, x)), ncnt(a, t))