Zulip Chat Archive

Stream: general

Topic: is this a typo?

Damiano Testa (Mar 01 2022 at 20:43):

https://github.com/leanprover-community/mathlib/blob/5e36e1213c246da906b002d4e608dc788871130c/src/tactic/norm_num.lean#L2

Damiano Testa (Mar 01 2022 at 20:44):

The author and copyright says Simon Hudon, which even autocorrects to Hudson on my phone. Is it a typo or is Simon Hudon really the author?

Adam Topaz (Mar 01 2022 at 20:44):

@Simon Hudon I think it's okay?

Damiano Testa (Mar 01 2022 at 20:48):

I feel the need to apologize for misreading the name all the time! I was convinced that there was an extra "s"! Sorry for the confusion!

Adam Topaz (Mar 01 2022 at 20:49):

I can't seem to find this Damiano Tesla though... ;)

Simon Hudon (Mar 01 2022 at 21:14):

No worries at all! I remember writing the first version of norm_num but the current version has probably been improved significantly since then

Yaël Dillies (Mar 01 2022 at 21:59):

Hudon is a French name, right?

Patrick Massot (Mar 01 2022 at 22:07):

Simon is from Québec.

Yaël Dillies (Mar 01 2022 at 22:11):

Ahah! Close enough

Yaël Dillies (Mar 01 2022 at 22:11):

I should've said francophone name

Last updated: Dec 20 2023 at 11:08 UTC