def positive_of

bendtorch-core@0.1.0.0 · src/storage/api.bend:718

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

718def positive_of(+n: Nat, +m: Nat, +over: {Nat.is_le(n, m) == False{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}:
719  match n:
720    case 0n:
721      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool},
722        Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(0n, m), False{}, Equal.sym(Bool, Nat.is_le(0n, m), True{}, Arith.le_zero(m)), over)))
723    case 1n+p:
724      {==}