Zulip Chat Archive

Stream: maths

Topic: does local increasing class instance depth break mathlib rul


view this post on Zulip Chris Hughes (Aug 13 2018 at 20:05):

So I'm doing Sylow's theorems in lean, and one of the proofs requires me to synthesize a fintype instance for the product of a subtype of a subtype of a finite type and a subtype of a quotient of a subtype of a finite type. This is complicated enough that the normal depth isn't good enough, but a deeper depth is good enough. Is it approved to increase the type class inference depth to deal with situations like these? The offending code is line 404 of https://github.com/dorhinj/mathlib/blob/sylow/group_theory/sylow.lean

view this post on Zulip Chris Hughes (Aug 13 2018 at 21:24):

Update. Proving one extra lemma has solved this problem.


Last updated: May 18 2021 at 08:14 UTC