`twoSum` の実装（HashMap を使用するバージョンとそうでないバージョンがある）

import Plausible
/- # 1. Two Sum

整数の配列 `nums` と整数 `target` が与えられたとき、合計が `target` になるような 2つの数のインデックス を返してください。
各入力には 必ずちょうど1つの解が存在する と仮定してかまいません。また、同じ要素を2回使ってはいけません。
答えは どちらの順番でも構いません。
-/

/-- 素朴な解法。for文を二重に回して解を探す。
for文を二重に回すため、計算量は`O(|nums|²)`になる。 -/
def naiveTwoSum (nums : List Int) (target : Int) : Option (Nat × Nat) := Id.run do
  let n := nums.length
  for i in [0:n] do
    for j in [i+1:n] do
      if nums[i]! + nums[j]! == target then
        return some (i, j)
  return none

#guard
  let nums := [2, 7, 11, 15]
  let target := 9
  let result := naiveTwoSum nums target |>.get!
  nums[result.fst]! + nums[result.snd]! == target

#guard
  let nums := [3, 2, 4]
  let target := 6
  let result := naiveTwoSum nums target |>.get!
  nums[result.fst]! + nums[result.snd]! == target

#guard
  let nums := [3, 3]
  let target := 6
  let result := naiveTwoSum nums target |>.get!
  nums[result.fst]! + nums[result.snd]! == target

open Std in

/-- 辞書を使った高速な実装。辞書からの検索は定数時間なので、計算量は`O(|nums|)`になる。 -/
def twoSum (nums : List Int) (target : Int) : Option (Nat × Nat) := Id.run do
  let mut map : HashMap Int Nat := Std.HashMap.emptyWithCapacity
  for (num, i) in nums.zipIdx do
    let complement := target - num
    if let some j := map[complement]? then
      return some (j, i)
    map := map.insert num i
  return none

#guard
  let nums := [0, -1, 3, 2, 13]
  let target := 2
  let result := twoSum nums target |>.get!
  nums[result.fst]! + nums[result.snd]! == target

namespace Test
  /- テスト -/

  /-- 長さ `n` で、中身の値が絶対値 `bound` 以下であるようなリストをランダム生成する -/
  def randList (n : Nat) (bound : Nat) : IO (List Int) := do
    let mut out := []
    for _ in [0 : n] do
      -- ランダムに 0 以上 bound 以下の自然数を生成する
      let x ← IO.rand 0 bound
      let pos ← IO.rand 0 1
      let y : Int := if pos == 0 then x else -x

      -- 生成した自然数をリストに追加する
      out := y :: out
    return out

  -- 長いリストを生成して、両者の計算時間を計測する
  #eval show IO Unit from do
    let nums ← randList 9000000 10000
    let start_time ← IO.monoMsNow
    let result1 := naiveTwoSum nums 100
    let end_time ← IO.monoMsNow
    IO.println s!"naiveTwoSum took {end_time - start_time} ms"
    match result1 with
    | none => IO.println "No solution found"
    | some (i, j) =>
      IO.println s!"Found solution: {i}, {j}"

    let start_time ← IO.monoMsNow
    let result2 := twoSum nums 100
    let end_time ← IO.monoMsNow
    IO.println s!"twoSum took {end_time - start_time} ms"
    match result2 with
    | none => IO.println "No solution found"
    | some (i, j) =>
      IO.println s!"Found solution: {i}, {j}"

end Test

Start by locating the example file associated with issue #1790 in the lean-by-example repository, then compare its surrounding structure with the supplied code. The issue provides naiveTwoSum, HashMap-based twoSum, #guard checks, and a benchmark; done means these examples are integrated in the appropriate location and the shown checks and evaluation run successfully.