def rank_naturals

bendtorch-core@0.1.0.0 · src/shape/core.bend:504

import Base

504def rank_naturals(+dims: List<&2, U32>) -> {rank_dimensions(dims) == List.length(&2, Nat, naturals(dims)) : Nat}:
505  match dims:
506    case Nil{}:
507      {==}
508    case head <> tail:
509      Equal.cong(Nat, Nat, value => 1n+value, rank_dimensions(tail), List.length(&2, Nat, naturals(tail)), rank_naturals(tail))