Discussion: Skolem award for the original Lean paper

Stream: general

[Floris van Doorn]

Discussion thread for #announce > Skolem award for the original Lean paper

[Kevin Buzzard]

But Lean 3 didn't stand the test of time! ;-)

[Kevin Buzzard]

More seriously, many congratulations! Here's to ten more years at least!

[Floris van Doorn]

And the paper was even further back, about Lean 2! Back in the days of higher-order unification (leading to incomprehensible error messages), the HoTT-mode instantiation of the kernel, Emacs as Lean's only editor, and a total user base that could be counted on 2-ish hands.

[Jeremy Avigad]

Ah, the good old days. And everything cost a nickel.

[Jakob von Raumer]

@Floris van Doorn Isn't one of the things that did survive from that era your proposal of mixing camel case and snake case in names?

[Floris van Doorn]

I had to refresh my memory: it seems that we mostly used snake case, even when defining new definitions or types. Some bundled categories used CamelCase. So I think the naming conventions were mostly those we used in Lean 3?