~/jendhub

def lt_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:55

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmp
import Base

55def lt_c(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
56  match c:
57    case LT{}:
58      {==}
59    case EQ{}:
60      absurd_tf({EQ{} == LT{} : Cmp}, h)
61    case GT{}:
62      absurd_tf({GT{} == LT{} : Cmp}, h)

Uses (4)

Used by (1)