Zulip Chat Archive

Stream: general

Topic: broke mathlib

Paul-Nicolas Madelaine (Jun 19 2019 at 09:36):

Hi everyone,

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: Aug 03 2023 at 10:10 UTC