:no_good: <Something> should not compare names

[favonia]

In #376, it was discovered that \<something> might be comparing names in Global.t that should be used purely for printing.

@jonsterling Seriously, what's wrong with us!!! :laughing:

[jonsterling]

i couldn't figure out where this is happening... a bit bizarre

[jonsterling]

I can confirm that conversion is not comparing names: https://github.com/RedPRL/cooltt/blob/main/src/core/Conversion.ml#L413

So it must be happening somewhere else... 😦

[favonia]

It could also be that we accidentally wrote sym0 = sym1 somewhere :scream:

[favonia]

The kado library looks okay. :thinking:

[jonsterling]

What about compare?

On Jun 5, 2022, at 5:49 PM, favonia @.***> wrote:

The kado library looks okay. 🤔

— Reply to this email directly, view it on GitHub https://github.com/RedPRL/cooltt/issues/377#issuecomment-1146837221, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAANOELC3UZRSMCEOAKETNDVNTD63ANCNFSM5X5GN5BA. You are receiving this because you were mentioned.

[favonia]

What about compare?

I found https://github.com/RedPRL/kado/pull/10 :rofl: but this should only affect efficiency

[favonia]

@jonsterling Okay, I think this is it?

https://github.com/RedPRL/cooltt/blob/7408368d8ee0076780f96e0907e959b31351cb65/src/core/Dim.ml#L12-L13