~/jendhub

def wn.lt_of

bend-osdev-word64@0.1.1.0 · proof_value.bend:218

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
import Base

218def wn.lt_of(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
219  match c:
220    case LT{}:
221      {==}
222    case EQ{}:
223      Empty.absurd({EQ{} == LT{} : Cmp}, wn.ft(e))
224    case GT{}:
225      Empty.absurd({GT{} == LT{} : Cmp}, wn.ft(e))

Uses (5)

Used by (1)