~/jendhub

def unique_failure

bendtorch-core@0.1.0.0 · src/tensor/permute_contract.bend:101

import bendtorch-core@0.1.0.0/src/tensor/permute_contract.bend as PermuteContract
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout

101def unique_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.unique(axes)>,
102  duplicate: {Layout.unique(axes) == False{} : Bool}) ->
103  {Layout.plan_unique(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
104  match decision:
105    case Shape.BFalse{no}:
106      {==}
107    case Shape.BTrue{yes}:
108      Empty.absurd({Layout.plan_unique(input, axes, Shape.BTrue{yes}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
109        Nats.contradiction(Layout.unique(axes), yes, Equal.sym(Bool, Layout.unique(axes), False{}, duplicate)))

Uses (13)

Used by (1)