def viewed_view

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:334

import Base
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend as Laws

334def viewed_view(+given: Slice.View, +s: Nat, +t: Nat, +p: Nat) ->
335  {Laws.view_part(Slice.viewed(given, s, t, p)) == view_pair(given) : Nat & Nat}:
336  match given:
337    case Slice.View{+o, +n, +i}:
338      {==}