def eq_half

bend-ml-tensor-array@0.1.19.0 · main.bend:1587

import Base

1587# the row counts of the two bands follow the row count of the node: if rr == r at run
1588# time, the same holds for both halves (the bands carry r only in their type)
1589def eq_half(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {half(a) == half(b) : Nat}:
1590  %e : {half(a) == half(_) : Nat}
1591  {==}