Doc-string error

Stream: CSLib

[Sorrachai Yingchareonthawornchai]

For this PR. The linter requires adding a docstring to a function. However, when a function is defined inside another function using where keyword, adding a docstring causes Lean to panic in some cases. Do you know how to fix this?

/-- If binary search returns an index, that index contains the search key. -/
private theorem binarySearch_index_correct (n : ℕ) (q : α) (arr : SortedArray α n) :
  ∀ i, (binarySearch arr q).ret = some i → arr[i] = q := by
    intro i hi
    apply aux n q 0 (n-1) (by omega)
    rw [binarySearch.eq_def] at hi
    exact hi
where /-- Panic here -/ aux (n : ℕ) (q : α) (a b : ℕ)
  (h_ab : a ≤ b) (arr : SortedArray α n) :
  ∀ i : ℕ, (binarySearch.bs_aux arr q a b h_ab).ret = some i → arr[i] = q := by {
    fun_induction binarySearch.bs_aux <;> all_goals (simp; split_ifs<;> grind)
  }

Header

PANIC at Lean.EnvExtension.modifyState Lean.Environment:1392:17: asyncDecl _private.Cslib.Algorithms.Lean.Searching.BinarySearch.0.Cslib.Algorithms.Lean.TimeM.binarySearch_index_correct.aux is outside current context Cslib.Algorithms.Lean.TimeM.binarySearch_index_correct

[Kyle Miller]

Please minimize the panic and report it as an issue to the Lean 4 repository!

[Chris Henson]

I have opened lean4#11799

[Notification Bot]

A message was moved here from #CSLib > SortedArray design (#247) by Chris Henson.

[Notification Bot]

2 messages were moved here from #CSLib > SortedArray design (#247) by Chris Henson.

[Kim Morrison]

Fixed in lean#11896