def lt_from

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:65

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

65def lt_from(+a: Nat, +b: Nat, below: {Nat.is_lt(a, b) == True{} : Bool}) -> Shape.LT(a, b):
66  match a b:
67    case 0n 0n:
68      Empty.absurd(Shape.LT(0n, 0n), Arith.clash(below))
69    case 0n 1n+q:
70      Unit{}
71    case 1n+p 0n:
72      Empty.absurd(Shape.LT(1n+p, 0n), Arith.clash(below))
73    case 1n+p 1n+q:
74      lt_from(p, q, below)