def lt_self_succ

bendtorch-core@0.1.0.0 · src/tensor/contracts/build_facts.bend:30

import Base

30def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
31  match k:
32    case 0n:
33      {==}
34    case 1n+p:
35      lt_self_succ(p)