LAWS.narrow_axis: law of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/LAWS.bend as LAWS
Lines 285-291 of bendtorch@1.3.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/LAWS.bend&start_line=285&end_line=291

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

# LAW (narrow_axis): narrowing axis d of a tensor that has it gives that axis exactly the length asked for.
law narrow_axis:
  for +s: List<&2, Nat>
  for +d: Nat
  for +l: Nat
  for e: {True{} == Nat.is_lt(d, TT.rank(s)) : Bool}
  {TT.at1(TT.setd(s, d, l), d) == l : Nat}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=at1
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=rank
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=setd