law permute_rank

bendtorch@1.3.0.0 · LAWS.bend:309

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

309# LAW (permute_rank): permuting by p gives as many axes as p has, so a permutation of the axes keeps the rank.
310law permute_rank:
311  for +s: List<&2, Nat>
312  for p: List<&2, Nat>
313  {TT.rank(TT.permuted(s, p)) == List.length(&2, Nat, p) : Nat}