def lt_step

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:74

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

74def lt_step(+position: Nat, +cursor: Nat, different: {False{} == Nat.is_eq(cursor, position) : Bool}) ->
75  {Nat.is_lt(position, cursor) == Nat.is_lt(position, 1n+cursor) : Bool}:
76  match position cursor:
77    case 0n 0n:
78      Empty.absurd({Nat.is_lt(0n, 0n) == Nat.is_lt(0n, 1n) : Bool}, Arith.clash(different))
79    case 0n 1n+bound:
80      {==}
81    case 1n+rest 0n:
82      below_one_more(rest)
83    case 1n+rest 1n+bound:
84      lt_step(rest, bound, different)