def pick_lt

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF

705def pick_lt(+c: Bool) -> {Nat.is_lt(SF.pick(Nat, c, 1n, 2n), 2047n) == True{} : Bool}:
706  match c:
707    case True{}:
708      {==}
709    case False{}:
710      {==}