def lt_irrefl

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

import Base

110def lt_irrefl(+x: Nat) -> {Nat.is_lt(x, x) == False{} : Bool}:
111  match x:
112    case 0n:
113      {==}
114    case 1n+p:
115      lt_irrefl(p)