Topic: broke mathlib
Paul-Nicolas Madelaine (Jun 19 2019 at 09:36):
I'm was working on fixing a problem with the norm_cast tactic, and it seems like I broke something in data/list.
The thing is, this part of the code doesn't use norm_cast, and doesn't seem to use coercion at all for that matter.
Plus, the error messages I get are about the equation compiler and pattern matching.
Could someone take a look and help me figure out what I'm looking at?
Here is the incriminated commit: https://github.com/leanprover-community/mathlib/pull/1103/commits/4daf46595da984c2947a771d269e9acd64b0afc1
Paul-Nicolas Madelaine (Jun 19 2019 at 12:19):
I created a dedicated thread in 'PR reviews', it seems more appropriate than the general stream
Last updated: May 16 2021 at 21:11 UTC