def wp.pick_lex

bend-osdev-word64@0.1.1.0 · PROOF.bend:68

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

68def wp.pick_lex(c: Cmp, -al: U32, -bl: U32) -> {W.W64.cmp.pick(c, al, bl) == P.wv.lex(c, U32.cmp(al, bl)) : Cmp}:
69  match c:
70    case LT{}:
71      {==}
72    case EQ{}:
73      {==}
74    case GT{}:
75      {==}