Yes, unfortunately, Lean is harder to search for than some other programming languages. Although it seems workable: both DuckDuckGo and Google return Lean-related top results for me for "lean induction" and "lean match expression," for example.
> And of course Coq is phallic both in English and the original French.
Is it phallic in French too? I am not a French speaker. According to the French Wiktionary, "coq" means rooster, male chicken, cooked rooster, male partridge, a self-important person, a rooster on top of a church bell tower, a loose coin, a tool used for ironing, a kind of fish, a part used in watchmaking, or a cook working on a ship.[1] None of these sound phallic to me.
I have not seen evidence that this was intended as an English pun. Rather, it seems to have been a double pun in French, for the calculus of constructions (CoC) which Coq is based on, and Thierry Coquand who developed CoC.[2] So I just assume that it wasn't meant to be phallic and remind myself that some people speak French and they name their software French names.
> And of course Coq is phallic both in English and the original French.
Is it phallic in French too? I am not a French speaker. According to the French Wiktionary, "coq" means rooster, male chicken, cooked rooster, male partridge, a self-important person, a rooster on top of a church bell tower, a loose coin, a tool used for ironing, a kind of fish, a part used in watchmaking, or a cook working on a ship.[1] None of these sound phallic to me.
I have not seen evidence that this was intended as an English pun. Rather, it seems to have been a double pun in French, for the calculus of constructions (CoC) which Coq is based on, and Thierry Coquand who developed CoC.[2] So I just assume that it wasn't meant to be phallic and remind myself that some people speak French and they name their software French names.
[1] https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194...
[2] https://github.com/coq/coq/wiki/Alternative-names