~/jendhub

def cm.le_of_lt

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

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

87def cm.le_of_lt(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}:
88  match c:
89    case LT{}:
90      {==}
91    case EQ{}:
92      Empty.absurd({True{} == True{} : Bool}, ab.ft(e))
93    case GT{}:
94      Empty.absurd({False{} == True{} : Bool}, ab.ft(e))

Uses (6)

Used by (1)