ConstructionPROOF.written_model: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
Lines 403-434 of bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&start_line=403&end_line=434

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof

def written_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
  +index: U32, +value: F32, -unit: Unit, -converted: {U32.to_nat(index) == cursor : Nat},
  -meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit}))) -> Written<shape, original, tensor, cursor, value>:
  Written{
    other => at =>
      {\{Tuple: checked => rest =>
        {\{Tuple: observed => frame => written_point(shape, tensor, cursor, index, value, converted, checked, observed, other, at)} :
          ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
            (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
              @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
                Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
                  {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
          (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
            {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(rest)
      } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
        (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
          {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(meaning),
    other => earlier => before_checked =>
      {\{Tuple: checked => rest =>
        {\{Tuple: observed => frame => frame(other)(before_checked)(
          %Equal.sym(Nat, U32.to_nat(index), cursor, converted) : {Nat.is_eq(_, U32.to_nat(other)) == False{} : Bool}
          CoreProof.lt_big_small_different(U32.to_nat(other), cursor, earlier))} :
          ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
            (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
              @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
                Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
                  {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
          (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
            {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(rest)
      } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
        (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
          {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(meaning)}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=Written
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=written_point
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=CheckedUpdateMeaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=ObservationChecked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=lt_big_small_different