def inner

bendtorch@1.3.0.0 · tensor.bend:264

import Base
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

264# the product of the sizes after axis k
265def inner(s: List<&2, Nat>, k: Nat) -> Nat:
266  match s k:
267    case Nil{} _:
268      1n
269    case Con{h, t} 0n:
270      NL.product(t)
271    case Con{h, t} 1n+p:
272      inner(t, p)