def le_lt_absurd

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:343

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

343def le_lt_absurd(+a: Nat, +b: Nat, le: {Nat.is_le(a, b) == True{} : Bool}, lt: {Nat.is_lt(b, a) == True{} : Bool}) -> Empty:
344  match a b:
345    case 0n b:
346      Arith.lt_zero(b, lt)
347    case 1n+p 0n:
348      Arith.clash(le)
349    case 1n+p 1n+q:
350      le_lt_absurd(p, q, le, lt)