ParentFull threadEthan_Barry·There was a hash collision bug in the main Lean kernel that was patched, but AFAIK nothing relied on it. You'd have to know what you were doing to accidentally get there...View on HN