has_reflect

Stream: lean4

[Chris Hughes]

Is there something like Lean3's has_reflect class in Lean 4?

[Gabriel Ebner]

You should avoid the built-in ToExpr class because it has a broken ToExpr Expr instance. I've written (and partly copied from Mario's code) a lawful Reflect alternative here: https://github.com/gebner/quote4/blob/8fd8422dfe2cd5d061754944ca345ffa6061781b/Qq/Reflect.lean

[Chris Hughes]

If I don't want to use ToExpr Expr is it okay to use the built in class?

[Gabriel Ebner]

If you want something quick, then sure. It's fine otherwise. I'd just avoid having [ToExpr α] anywhere (since you could get the ToExpr Expr class accidentally).