def lt_from

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_proof.bend:97

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

97def lt_from(+a: Nat, +b: Nat, below: {Nat.is_lt(a, b) == True{} : Bool}) -> Shape.LT(a, b):
98  match a b:
99    case 0n 0n:
100      Empty.absurd(Shape.LT(0n, 0n), Arith.clash(below))
101    case 0n 1n+q:
102      Unit{}
103    case 1n+p 0n:
104      Empty.absurd(Shape.LT(1n+p, 0n), Arith.clash(below))
105    case 1n+p 1n+q:
106      lt_from(p, q, below)