🙅 <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!!! 😆

[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 😱

[favonia]

The kado library looks okay. 🤔

[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 <#377 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAANOELC3UZRSMCEOAKETNDVNTD63ANCNFSM5X5GN5BA>. You are receiving this because you were mentioned.

[favonia]

What about compare?

I found RedPRL/kado#10 🤣 but this should only affect efficiency

[favonia]

@jonsterling Okay, I think this is it?

cooltt/src/core/Dim.ml

Lines 12 to 13 in 7408368

	let equal : t -> t -> bool = (=)
	let compare : t -> t -> int = compare