~/jendhub

def cm.eq_of_le

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

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

96# is_le(c) and not is_lt(c): c is EQ
97def cm.eq_of_le(c: Cmp, +e: {Cmp.is_le(c) == True{} : Bool}, +f: {Cmp.is_lt(c) == False{} : Bool}) -> {c == EQ{} : Cmp}:
98  match c:
99    case LT{}:
100      Empty.absurd({LT{} == EQ{} : Cmp}, ab.tf(f))
101    case EQ{}:
102      {==}
103    case GT{}:
104      Empty.absurd({GT{} == EQ{} : Cmp}, ab.ft(e))

Uses (7)

Used by (1)