def fin_order

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:34

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U

34def fin_order(+x: Bool, +y: Bool, +c: Cmp, +d: Cmp) -> {Word.cmp.fin(x, y, U.order(c, d)) == U.order(c, Word.cmp.fin(x, y, d)) : Cmp}:
35  match c:
36    case LT{}:
37      {==}
38    case EQ{}:
39      {==}
40    case GT{}:
41      {==}