mathlib
5b154e45 - Fix timeout due to elaborator confusion

Commit
4 years ago
Fix timeout due to elaborator confusion (This was also extremely slow on master.) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Dot.20notation.20mysteriously.20speeds.20up.20elaborator
Author
Parents
Loading