def cmp_code

bend-collections-laws-math@1.0.0.0 · proofs/lib/logic.bend:58

import Base

58# Cmp discrimination.
59def cmp_code(c: Cmp) -> Nat:
60  match c:
61    case LT{}:
62      0n
63    case EQ{}:
64      1n
65    case GT{}:
66      2n