## Stream: new members

### Topic: maximum class-instance resolution depth has been reached

#### Kris Brown (Jun 18 2020 at 01:37):

I'm trying to prove a theorem related to permutations of finite sets. At the beginning (trying to define a predicate on permutations to assert they are cyclic) and running into an issue that I don't know how to debug. The error (which is on the very last x of the very last definition) is "maximum class-instance resolution depth has been reached". I tried restarting Lean, setting class.instance_max_depth 1000, and I turned on trace.class_instances, though that spits out something extremely long that I can't make sense of. How should I approach this error, as a beginner?

import data.equiv.basic
import data.finset

open equiv -- "perm x" is "equiv x x" AKA "x ≃ x"
open nat

-- Repeat a binary function n times
def rep {α : Type*} : ℕ → (α → α) → α → α
| 0 _ x := x
| (succ n) f x := f (rep n f x)

-- Π (n : ℕ), perm (fin n) → fin n → fin n
#check λ (n:ℕ) (p: perm (fin n)) (x: fin n),
rep n p.to_fun x

-- Predicate for a permutation on a finite set to be cyclic
def cyclic {n : ℕ} (p : perm (fin n)) :=
∃ x : fin n, rep n p.to_fun x = x


#### Jalex Stark (Jun 18 2020 at 01:38):

put a newline after your backticks tog et syntax highlighting

#### Jalex Stark (Jun 18 2020 at 01:39):

i don't get any error

#### Jalex Stark (Jun 18 2020 at 01:41):

you should change your instance_max_depth back to default, this may cause slowdowns for you later

#### Kris Brown (Jun 18 2020 at 01:42):

Thanks! and that's interesting; I'm using Lean 3.4.2 - are there any candidates for settings I could change to match your setup?

#### Jalex Stark (Jun 18 2020 at 01:43):

around here the suggestion is to use that latest leanprover-community build with the latest mathlib

#### Jalex Stark (Jun 18 2020 at 01:43):

managing that installation is easy with the leanproject tool

#### Jalex Stark (Jun 18 2020 at 01:44):

https://leanprover-community.github.io/get_started.html

#### Jalex Stark (Jun 18 2020 at 01:46):

you can use the lean web editor in the meantime

web editor

#### Scott Morrison (Jun 18 2020 at 01:52):

3.4.2 is pretty old by now (it's the last "official" release before switching to community development), and in particular is missing lots of nice improvements to the typeclass search algorithm.