def cnt1

minebender-game@1.0.0.0 · proof_gen.bend:914

import Base

914# How many elements of xs are one below a.
915def cnt1(+a: Nat, xs: List<&2, Nat>) -> Nat:
916  match xs:
917    case Nil{}:
918      0n
919    case x <> t:
920      Nat.add(one(Nat.is_eq(1n+x, a)), cnt1(a, t))