~/jendhub

def ab.lt_eqc

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:311

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
import Base

311def ab.lt_eqc(c: Cmp, +h: {c == EQ{} : Cmp}, +e: {Cmp.is_lt(c) == True{} : Bool}) -> Empty:
312  match c:
313    case LT{}:
314      ab.lt_eq(h)
315    case EQ{}:
316      ab.ft(e)
317    case GT{}:
318      ab.gt_eq(h)

Uses (7)

Used by (1)