Zulip Chat Archive
Stream: lean4
Topic: trace.Compiler.simp v trace.compiler.simp
Kevin Buzzard (Dec 07 2024 at 23:47):
Both of these seem to exist. Is this intentional?
Mario Carneiro (Dec 08 2024 at 04:40):
they are different traces :upside_down: The capitalized one is the new compiler
Last updated: May 02 2025 at 03:31 UTC