Zulip Chat Archive

Stream: mathlib4

Topic: ext.1

Kevin Buzzard (Nov 29 2022 at 22:51):

Why did mathlib3port change @[ext] here to @[ext.1] here? (note that @[ext.1] gives an error, and @[ext] seems to work fine in mathlib4)

Gabriel Ebner (Nov 29 2022 at 23:02):

This is an interesting bug!

Kevin Buzzard (Nov 29 2022 at 23:17):

it's heartening (and perhaps a little surprising) to know that my stream of naive questions every time I attempt to port a file aren't all completely uninteresting!

Gabriel Ebner (Nov 29 2022 at 23:31):

Yet another case where simple attributes make things anything but simple. https://github.com/leanprover-community/mathport/commit/e2277bc26878a182b99e26ed135c2e6e780b1f1f

Mario Carneiro (Nov 30 2022 at 00:15):

Oh I see, this was silent breakage when syntax "ext" (ident)? : attr was removed

Last updated: Dec 20 2023 at 11:08 UTC