def plan_construct
bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:9
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
9def plan_construct(+left: Shape.Shape, +right: Shape.Shape, -left_padding: Nat, -right_padding: Nat, -minimal: Shape.PadMinimal<left_padding, right_padding>, -output: List<&2, U32>, -aligned: Shape.Aligned(Shape.pad(left_padding, Shape.extents(left)), Shape.pad(right_padding, Shape.extents(right)), Shape.naturals(output)), +result: Shape.ConstructResult<output>) -> {Laws.planned_dimensions(left, right, Shape.broadcast_checked.construct(left, right, left_padding, right_padding, minimal, output, aligned, result)) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}:
10 match result:
11 case Shape.SError{error}:
12 {==}
13 case Shape.SBuilt{shape, preserved}:
14 {==}