~/jendhub

def eq_c

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

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

64def eq_c(+c: Cmp, +h: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
65  match c:
66    case LT{}:
67      absurd_tf({LT{} == EQ{} : Cmp}, h)
68    case EQ{}:
69      {==}
70    case GT{}:
71      absurd_tf({GT{} == EQ{} : Cmp}, h)

Uses (4)

Used by (1)