def positive_of

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:166

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

166def positive_of(+t: Nat, +a: Nat, +size: Nat, below: {Nat.is_lt(t, Nat.mul(a, size)) == True{} : Bool}) ->
167  {Nat.is_lt(0n, size) == True{} : Bool}:
168  match size:
169    case 0n:
170      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool},
171        Arith.lt_zero(t,
172          %Nats.mul_zero_right(a) : {Nat.is_lt(t, _) == True{} : Bool}
173          below))
174    case 1n+p:
175      {==}