~/jendhub

def lt_self_successor

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:194

import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

194def lt_self_successor(number: Nat) -> Shape.LT(number, 1n+number):
195  match number:
196    case 0n:
197      Unit{}
198    case 1n+p:
199      lt_self_successor(p)

Uses (3)

Used by (1)