def tl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:134

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

134# the sticky bit merges the parity bit with "some lower bit is set"
135def tl(+b: Nat, +l: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {NC.lex(Nat.cmp(b, 0n), Nat.cmp(l, 0n)) == Nat.cmp(Nat.max(b, Nat.min(l, 1n)), 0n) : Cmp}:
136  match b l:
137    case 0n 0n:
138      {==}
139    case 0n 1n+ +lp:
140      {==}
141    case 1n 0n:
142      {==}
143    case 1n 1n+ +lp:
144      {==}
145    case 2n+ +q _:
146      NC.absurd_tf({NC.lex(Nat.cmp(2n+q, 0n), Nat.cmp(l, 0n)) == Nat.cmp(Nat.max(2n+q, Nat.min(l, 1n)), 0n) : Cmp}, hb)