{"request":{"endpoint":"https://exercism.org/api/v2/tracks/lean/exercises/binary-search/community_solutions","query":{},"options":{"initial_data":{"results":[{"uuid":"2a7ce4d6b2d842898a660068959f71ad","snippet":"def find (value : Int) (array : Array Int) : Option Nat := Id.run do let mut low := 0 let mut high := array.size while low < high do let middle := (low + high) / 2 let element := array[middle]! if value < element then high := middle if value > element then low := middle + 1 if value == element then return some middle none ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":2,"num_iterations":1,"num_loc":12,"iteration_status":"analyzing","published_iteration_head_tests_status":"passed","published_at":"2026-02-07T11:12:37.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"keiraville"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/keiraville","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"1c196cc935e242c2992a095006380fc8","snippet":"namespace BinarySearch def search (value : Int) (array : Array Int) (low : Fin array.size) (high : Fin array.size) : Option Nat := let mid := (low.val + high.val) / 2 match compare value array[mid] with | .eq => some mid | .gt => -- mid < high.val -> mid + 1 <= high.val < array.size (by Fin property) if SuccMidFin : mid < high.val then search value array ⟨mid + 1, by grind⟩ high ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":19,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-01-26T16:21:46.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"oxe-b"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/oxe-b","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"3dd7b5db946e487a90c00f86fc59452b","snippet":"def find (value : Int) (array : Array Int) : Option Nat := let rec loop (low high : Nat) : Option Nat := if low < high then let m := (high + low) / 2 let m_val := array[m]! if value < m_val then loop low m else if value > m_val then loop (m + 1) high else ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":16,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-04-06T10:56:59.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"takah29"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/takah29","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"3615c4aabb8a41d5abb624f6a6e172f0","snippet":"def find (value : Int) (array : Array Int) : Option Nat := loop 0 array.size where loop (lo hi : Nat) : Option Nat := if lo >= hi then none else let mid := (lo + hi) / 2 match compare array[mid]! value with | .eq => some mid ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":14,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-05-14T02:49:45.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"jinwoo"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/jinwoo","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"727b3144a4c849f98dd7109614a73d42","snippet":"def find (value : Int) (array : Array Int) : Option Nat := Id.run do let mut lo := 0 let mut hi := array.size while lo < hi do let mid := (lo + hi) / 2 if value < array[mid]! then hi := mid else if value > array[mid]! then lo := mid + 1 else return some mid none ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":11,"iteration_status":"analyzing","published_iteration_head_tests_status":"passed","published_at":"2026-03-31T20:57:00.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"menketechnologies"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/menketechnologies","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"8e9a28b9ee4540439d1706e31a0dd682","snippet":"@[inline] partial def find (value : Int) (array : Array Int) : Option Nat := let rec go (left right : Nat) : Option Nat := if left < right then let mid := (left + right) / 2 let x := array[mid]! if x == value then some mid else if x < value then go (mid + 1) right ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":17,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-05-20T16:18:28.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"david82"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/david82","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"1b23ac00233441c3855bc917528d8422","snippet":"def find (value : Int) (array : Array Int) : Option Nat := go 0 array.size where go (l h : Nat) : Option Nat := do if l < h then let m := (l + h) / 2 match compare value array[m]! with | .lt => go l m | .eq => some m | .gt => go (m + 1) h else ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":13,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-05-28T07:00:11.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"setsunica"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/setsunica","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"eeb24470f7484bfcb59104cf980537e5","snippet":"def f (value : Int) (array : Array Int) (left : Nat) (right : Nat) (hl : left < array.size) (hr : right < array.size) : Option Nat := if left >= right then if array[left] == value then some left else none else let middle := (left + right + 1) / 2 if array[middle] <= value then f value array middle right (by omega) (by omega) else f value array left (middle - 1) (by omega) (by omega) ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":15,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-08-22T21:04:59.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"ramhuw"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/ramhuw","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"381e4a053ebc485abab94111f9745c9b","snippet":"def find (value : Int) (array : Array Int) : Option Nat := Id.run do if array.isEmpty then return none let mut low := 0 let mut high := array.size while low < high do let mid := low + (high - low) / 2 let a := array[mid]! ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":17,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-06-06T09:45:25.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"grixb"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/grixb","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}},{"uuid":"62b254f5da324826a0aea087832036b1","snippet":"partial def find_helper (value : Int) (array : Array Int) (start_ind : Int) (end_ind : Int) : Option Nat := if end_ind < start_ind then none else let mid_idx := (end_ind + start_ind) / 2 let mid_elem := array[mid_idx.toNat]? match mid_elem with | none => none | some mid_elem_val => if mid_elem_val == value then ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":19,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-08-23T00:28:40.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"sgomber"},"exercise":{"title":"جست‌وجوی دودویی","icon_url":"https://assets.exercism.org/exercises/binary-search.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/solutions/sgomber","private_iterations_url":"https://exercism.org/fa/tracks/lean/exercises/binary-search/iterations"}}],"meta":{"current_page":1,"total_count":10,"total_pages":1,"unscoped_total":10}}}}}

مسیرهای زبان

با Jiki کدنویسی یاد بگیرید

سفر شما

علاقه‌مندی‌های شماجدید

مزایای Exercism

ویدیوهای جامعه

مجموعه‌ی معرفی‌های کوتاه

مصاحبه‌ها و داستان‌ها

Discord

انجمن

شروع کار

منتورینگ

مستندات

مشارکت‌کنندگان

مترجمانجدید

حمایت مالی

درباره‌ی Exercism

تأثیر ما

همگام‌ساز GitHubجدید

Insiders