def wd.fin_flip

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:215

import Base

215def wd.fin_flip(c: Cmp, x: Bool, y: Bool) -> {Word.cmp.fin(y, x, cm.flip(c)) == cm.flip(Word.cmp.fin(x, y, c)) : Cmp}:
216  match c:
217    case LT{}:
218      {==}
219    case EQ{}:
220      wd.bool_flip(x, y)
221    case GT{}:
222      {==}