def cm.lt_of

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

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

import Base

74def cm.lt_of(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
75  match c:
76    case LT{}:
77      {==}
78    case EQ{}:
79      Empty.absurd({EQ{} == LT{} : Cmp}, ab.ft(e))
80    case GT{}:
81      Empty.absurd({GT{} == LT{} : Cmp}, ab.ft(e))

Uses (5)

Used by (3)