Lean4

34. Binary search

EasyProgramFree10 points

nums is an array of distinct integers in increasing order. Write search nums target, which returns some i when nums[i] = target and none when target is not in the array.

The hidden tests search a 20,000-element array 40,000 times, so reading the array from the start on every search will run out of time.

Examples

  1. Inputsearch #[-1, 0, 3, 5, 9, 12] 9Outputsome 4
  2. Inputsearch #[-1, 0, 3, 5, 9, 12] 2Outputnone

Submitting also runs 9 hidden tests.

arrayssearchperformance

Learn the ideas

Similar problems

Solution.lean
Loading…
Loading editor…
3#guard (search #[-1, 0, 3, 5, 9, 12] 9) = (some 4)
4#guard (search #[-1, 0, 3, 5, 9, 12] 2) = (none)
examples

Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.

ReadyLn 1, Col 1Lean 4
Draft saved in this browser