~/jendhub

def plan_align

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:16

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

16def plan_align(+left: Shape.Shape, +right: Shape.Shape, +left_padding: Nat, +right_padding: Nat, -minimal: Shape.PadMinimal<left_padding, right_padding>, +alignment: Shape.Alignment<Shape.pad_words(left_padding, Shape.dimensions(left)), Shape.pad_words(right_padding, Shape.dimensions(right))>) -> {Laws.planned_dimensions(left, right, Shape.broadcast_checked.align(left, right, left_padding, right_padding, minimal, alignment)) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}:
17  match alignment:
18    case Shape.Misaligned{}:
19      {==}
20    case Shape.Aligns{+output, aligned}:
21      plan_construct(left, right, left_padding, right_padding, minimal, output, Shape.broadcast_checked.repad(left_padding, right_padding, Shape.dimensions(left), Shape.dimensions(right), output, aligned), Shape.construct(output))

Uses (15)

Used by (1)