def aligned_length_right

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

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

119def aligned_length_right(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Aligned(left, right, output)) -> {List.length(&2, Nat, right) == List.length(&2, Nat, output) : Nat}:
120  match left right output:
121    case Nil{} Nil{} Nil{}:
122      {==}
123    case +lh <> +lt +rh <> +rt +oh <> +ot:
124      Shape.AStep{axis, +tail} = alignment
125      %aligned_length_right(lt, rt, ot, tail) : {1n+List.length(&2, Nat, rt) == 1n+_ : Nat}
126      {==}
127    case Nil{} Nil{} oh <> ot:
128      match alignment:
129    case Nil{} rh <> rt Nil{}:
130      match alignment:
131    case lh <> lt Nil{} Nil{}:
132      match alignment:
133    case Nil{} rh <> rt oh <> ot:
134      match alignment:
135    case lh <> lt Nil{} oh <> ot:
136      match alignment:
137    case lh <> lt rh <> rt Nil{}:
138      match alignment: