IndisputableMonolith.Compat.FunctionIterate

   1import Mathlib
   2
   3/-!
   4# IndisputableMonolith.Compat.FunctionIterate
   5
   6Lean/Mathlib versions differ on whether `Function.iterate` exists.
   7This repo historically used `Function.iterate` in a number of files.
   8
   9In current Mathlib, the canonical API is `Nat.iterate` / the notation `f^[n]`.
  10This module provides a tiny **compatibility shim** so older code continues to compile.
  11-/
  12
  13namespace Function
  14
  15universe u
  16variable {α : Sort u}
  17
  18/-- Compatibility definition: iterate `f` for `n` steps starting from `a`. -/
  19def iterate (f : α → α) (n : Nat) (a : α) : α :=
  20  Nat.iterate f n a
  21
  22end Function
  23