I just spilled my coffee; sorry for the trivial remark, but the name means 'pubic hairs' in Romanian. Apologies.. I thought it's better for you to know and ignore than not to (not quite a big population target for you, I imagine, anyway).
As Coq (now Rcoq) found to their chagrin... I'm convinced half of the reason Lean has surpassed Coq in mindshare in formal mathematics was because it's impossible to not chuckle at the name sometimes.
huffer · · focus · HN ↗
nxobject · · focus · HN ↗