def lt_extend
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:201
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
201def lt_extend(+number: Nat, +bound: Nat, proof: Shape.LT(number, bound)) -> Shape.LT(number, 1n+bound):
202 match number bound:
203 case 0n 0n:
204 match proof:
205 case 0n 1n+p:
206 Unit{}
207 case 1n+p 0n:
208 match proof:
209 case 1n+p 1n+q:
210 lt_extend(p, q, proof)