def aligned_length_left

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

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

98def aligned_length_left(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Aligned(left, right, output)) -> {List.length(&2, Nat, left) == List.length(&2, Nat, output) : Nat}:
99  match left right output:
100    case Nil{} Nil{} Nil{}:
101      {==}
102    case +lh <> +lt +rh <> +rt +oh <> +ot:
103      Shape.AStep{axis, +tail} = alignment
104      %aligned_length_left(lt, rt, ot, tail) : {1n+List.length(&2, Nat, lt) == 1n+_ : Nat}
105      {==}
106    case Nil{} Nil{} oh <> ot:
107      match alignment:
108    case Nil{} rh <> rt Nil{}:
109      match alignment:
110    case lh <> lt Nil{} Nil{}:
111      match alignment:
112    case Nil{} rh <> rt oh <> ot:
113      match alignment:
114    case lh <> lt Nil{} oh <> ot:
115      match alignment:
116    case lh <> lt rh <> rt Nil{}:
117      match alignment: