def digits_length

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

87def digits_length(+dims: List<&2, Nat>, +index: Nat) -> {List.length(&2, Nat, Shape.digits(dims, index)) == List.length(&2, Nat, dims) : Nat}:
88  match dims:
89    case Nil{}:
90      {==}
91    case head <> +tail:
92      Equal.cong(Nat, Nat, value => 1n+value, List.length(&2, Nat, Shape.digits(tail, Nat.mod(index, Shape.numel(tail)))), List.length(&2, Nat, tail), digits_length(tail, Nat.mod(index, Shape.numel(tail))))