fix: macro scopes in Conv.congr #1955
Conversation
|
Missing test output? |
|
it takes me 20 minutes to compile and run the test anyway... I believe the test should result in no change to the output so I'm just optimistically running CI. (If the test fails then a panic message will be produced.) |
|
Ah, wouldn't it be nicer though to also test that the goal tag looks as expected? |
|
Well it's a hygienic name, so it's hard to test that it has the right scopes. This is an edge case anyway, so I'm happy as long as it doesn't panic. |
|
It's not hygiened anymore after |
|
it should still be hygienic, with the same macro scopes as the original case tag. The bug occurs when you have both a hygienic base tag and want to append a hygienic field name to it. With the fix, the field name is no longer hygienic but the base tag still is, so you get a hygienic result. |
|
No, I don't think goal tags are supposed to ever be hygienic, that's why |
As reported on Zulip.