{"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/hi/tracks/lean/exercises/binary-search/solutions/keiraville","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/oxe-b","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/takah29","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/jinwoo","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/menketechnologies","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/david82","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/setsunica","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/ramhuw","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/grixb","private_iterations_url":"https://exercism.org/hi/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/hi/tracks/lean/exercises/binary-search/solutions/sgomber","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/binary-search/iterations"}}],"meta":{"current_page":1,"total_count":10,"total_pages":1,"unscoped_total":10}}}}}

भाषा ट्रैक

Jiki के साथ कोड करना सीखिए

आपकी यात्रा

आपके पसंदीदानया

Exercism के खास फायदे

कम्युनिटी वीडियो

संक्षिप्त परिचय शृंखला

इंटरव्यू और कहानियाँ

Discord

फोरम

शुरुआत करें

मेंटर बनें

डॉक्स

योगदानकर्ता

अनुवादकनया

दान करें

Exercism के बारे में

हमारा प्रभाव

GitHub सिंकरनया

इनसाइडर्स