Lean4

4. Two sum

MediumProgramAcademy Pass20 points

Given a list of integers nums and a target, write twoSum nums target. It returns some (i, j) when i < j and the elements at positions i and j add up to target, and none when no such pair exists. Positions count from 0.

When several pairs work, return the one with the smallest i, and among those the smallest j.

Examples

  1. InputtwoSum [2, 7, 11, 15] 9Outputsome (0, 1)
  2. InputtwoSum [3, 2, 4] 6Outputsome (1, 2)
  3. InputtwoSum [1, 2] 7Outputnone

Submitting also runs 8 hidden tests.

Constraints

  • Hidden tests include negative numbers, repeated values and lists of 200 elements.
listsarrayssearch

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Learn the ideas

Similar problems

Solution.lean
Loading…
Loading editor…
3#guard (twoSum [2, 7, 11, 15] 9) = (some (0, 1))
4#guard (twoSum [3, 2, 4] 6) = (some (1, 2))
5#guard (twoSum [1, 2] 7) = (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