The setting is a tutorial on program verification in Agda. Please consult the programme for further details. [ See also Appendix A .]

@article{paperbot3330,
  title = {Binary search—think positive},
  author = {ALEXANDER DINGES and RALF HINZE},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s0956796825000061}
}