`Std.Range` はダメ、`Std.Rco` などを使うべき

import Lean

open Std

variable {α : Type} [Inhabited α] [LE α] [LT α]
variable [DecidableLE α] [DecidableLT α]
variable [IsLinearOrder α]

@[grind =]
theorem Range_mem_iff_Range_toList (range : Range) (i : Nat) : i ∈ range ↔ i ∈ range.toList := by
  sorry

def isSorted (l : Array α) : Bool := Id.run do
  let n := l.size
  for h : i in [1:n] do
    if l[i-1]'(by grind) > l[i] then
      return false
  return true

上記の sorry を埋められなくて困っていた。これは、Std.Range を使用しているのがよくない。

次は通る。

import Std

open Std

variable {α : Type} [Inhabited α] [LE α] [LT α]
variable [DecidableLE α] [DecidableLT α]
variable [IsLinearOrder α]

def isSorted (l : Array α) : Bool := Id.run do
  let n := l.size
  for h : i in 1...n do
    if l[i-1] > l[i] then
      return false
  return true

Search the repository for the Range_mem_iff_Range_toList theorem and the isSorted example shown here. Read the surrounding example to determine which range notation is intended, then update the affected documentation example and verify that it compiles without the reported range-related issue.