type RetainedFailure

bendtorch-core@0.1.0.0 · src/tensor/transform_records.bend:6

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/transform_observation.bend as Observation

6type RetainedFailure<-input: Shape.Shape, -fill: F32, -request: Observation.Request, -code: U32> is Type:
7  RetainedFailure{
8    outcome: {Observation.failure_code(input, request, Core.new(input, fill)) == Some{code} : Maybe<&2, U32>},
9    retained_dimensions: {Observation.kept_dimensions(input, request, Core.new(input, fill)) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
10    retained_count: {Observation.kept_length(input, request, Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
11    retained_word_count: {Observation.kept_count(input, request, Core.new(input, fill)) == Some{Shape.count(input)} : Maybe<&2, U32>},
12    retained_value: @+other: U32 -> @inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool} ->
13      {Observation.kept_value(input, request, other, Core.new(input, fill)) == Some{fill} : Maybe<&2, F32>}}