Zulip Chat Archive

Stream: lean4

Topic: Mu symbol

Marcus Rossel (Oct 08 2022 at 08:04):

The following definition fails:

def µ := 0

with expected token as error on µ.
Is this intentional?

Sebastian Ullrich (Oct 08 2022 at 08:15):

That's not a GREEK SMALL LETTER MU but MICRO SIGN

Sebastian Ullrich (Oct 08 2022 at 08:18):

This is the current list of Approved Letters: https://github.com/leanprover/lean4/blob/ee603ab741db5e5462135df3ad2a8745857b71c6/src/Init/Meta.lean#L71-L77

Last updated: Dec 20 2023 at 11:08 UTC