def positive_of_lt

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:336

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

336def positive_of_lt(+w: Nat, +n: Nat, h: {Nat.is_lt(w, n) == True{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}:
337  match n:
338    case 0n:
339      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.lt_zero(w, h))
340    case 1n+q:
341      {==}