Zulip Chat Archive

Stream: lean4

Topic: Is seeing sorryAx a bug?


view this post on Zulip Jason Gross (Mar 11 2021 at 20:01):

Is it a bug if I get error messages mentioning sorry when I haven't used sorry myself?

instance has_arr : HasArr Preorder := { Arr := Function }
-- unknown identifier 'HasArr'
-- invalid {...} notation, 'sorryAx' is not a structure

view this post on Zulip Leonardo de Moura (Mar 11 2021 at 20:19):

I just pushed a fix for this issue.
We have a mechanism for suppressing error messages mentioning "synthetic sorry"s. It failed in this error message because it contained a name/string instead of an expression. It is fixed now.


Last updated: May 18 2021 at 22:15 UTC