Unexpected token when deriving instance

Stream: new members

[Benjamin]

The following code gives me an error on the final line:

import Lean
import Mathlib.Data.Rat.Init

#check ℚ
deriving instance Lean.ToExpr for ℚ

I get the error unexpected token 'ℚ'; expected identifier.

How can I fix this?

[Aaron Liu]

deriving instance Lean.ToExpr for Rat

[Benjamin]

This gives me an error typeclass instance problem is stuck, it is often due to metavariables.

[Aaron Liu]

Well, then I have run out of ideas, you can still write the instance manually

[Notification Bot]

16 messages were moved from this topic to #Is there code for X? > Lean.ToExpr Rat by Eric Wieser.