def lt_true

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:20

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

20def lt_true(+a: Nat, +b: Nat, bound: Shape.LT(a, b)) -> {True{} == Nat.is_lt(a, b) : Bool}:
21  match a b:
22    case 0n 0n:
23      match bound:
24    case 0n 1n+q:
25      {==}
26    case 1n+p 0n:
27      match bound:
28    case 1n+p 1n+q:
29      lt_true(p, q, bound)