def dot_zeros

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

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

73def dot_zeros(+count: Nat, +values: List<&2, Nat>, +steps: List<&2, Nat>) -> {dot(zeros(count, steps), values) == dot(steps, List.drop(&2, Nat, values, count)) : Nat}:
74  match count values:
75    case 0n values:
76      %Broadcast.drop_zero(values) : {dot(steps, values) == dot(steps, _) : Nat}
77      {==}
78    case 1n+rest Nil{}:
79      match steps:
80        case Nil{}:
81          {==}
82        case head <> tail:
83          {==}
84    case 1n+rest +value <> +tail:
85      dot_zeros(rest, tail, steps)