def lt_one

bendtorch-core@0.1.0.0 · src/storage/arith.bend:333

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

import Base

333def lt_one(+x: Nat, h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {0n == x : Nat}:
334  match x:
335    case 0n:
336      {==}
337    case 1n+p:
338      Empty.absurd({0n == 1n+p : Nat}, lt_zero(p, h))

Uses (5)

Used by (2)