def lt_zero

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

import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs

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

100def lt_zero(+a: Nat, bound: Shape.LT(a, 0n)) -> Empty:
101  match a:
102    case 0n:
103      match bound:
104    case 1n+p:
105      match bound:

Uses (3)

Used by (2)