def start_room
bendtorch-core@0.1.0.0 · src/tensor/from_values_contract.bend:288
import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValuesContract
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
288def start_room(+shape: Shape.Shape, +values: List<&2, F32>,
289 +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
290 {Nat.is_le(Nat.add(0n, List.length(&2, F32, values)), U32.to_nat(Shape.count(shape))) == True{} : Bool}:
291 %Equal.sym(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), counted) :
292 {Nat.is_le(_, U32.to_nat(Shape.count(shape))) == True{} : Bool}
293 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
294 {Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), _) == True{} : Bool}
295 Api.le_refl(Shape.logical_numel(Shape.dimensions(shape)))