How to use non-ASCII characters as identifiers?

[hhiim]

I have tried using non-ASCII characters as the name of axioms (such as Chinese characters), but Lean gives an error: "expected token".

def 字符串:="this is a string"

Is there any feasible solution? (However, it is possible to use fancy characters, such as ℙ)

[Martin-Molinero]

Hey @hhiim!

Believe def 字符串:="this is a string" is not a valid syntax, at least in py 3.11. The following code works correctly in the QC cloud:

class CalculatingRedOrangeBuffalo(QCAlgorithm):
    def Initialize(self):
        self.Quit(self.字符串())

    def 字符串(self):
        return "this is a string"

[hhiim]

Hey @hhiim!

Believe def 字符串:="this is a string" is not a valid syntax, at least in py 3.11. The following code works correctly in the QC cloud:

class CalculatingRedOrangeBuffalo(QCAlgorithm):
    def Initialize(self):
        self.Quit(self.字符串())

    def 字符串(self):
        return "this is a string"

Sorry, It's a misunderstanding. I was not distinguishing "Lean" and "Lean Theorem Prover"... close the question please --- again sorry!