def bc_eq

bendtorch@1.3.0.0 · tensor.bend:74

import Base

74# three shapes of one rank, axis by axis
75def bc_eq(a: List<&2, Nat>, b: List<&2, Nat>, o: List<&2, Nat>) -> Bool:
76  match a b o:
77    case Nil{} Nil{} Nil{}:
78      True{}
79    case Con{+x, ra} Con{+y, rb} Con{+z, ro}:
80      # bend-lint: disable-next bend-lint-rules/performance/eager_branch -- a shape predicate over a list of rank <= 4, once per operation; the types and LAWS.bend read its Bool form not-expected-because: a match would change the definition the proofs reduce, for no measurable gain
81      Bool.and(bc_dim(x, y, z), bc_eq(ra, rb, ro))
82    case _ _ _:
83      False{}