I am interested in debugging the NormCastExt extension to better understand how it works (https://github.com/leanprover/std4/blob/5aa4ab4f0c096e8d0600e3ae41b8577dcf6edb13/Std/Tactic/NormCast/Ext.lean#L108). I'd like to print out the values of the instance Std.Tactic.NormCast.normCastExt
in order to see what it's value is:
import Std.Tactic.NormCast.Ext
#eval Std.Tactic.NormCast.normCastExt
But it doesn't seem printable:
expression
Std.Tactic.NormCast.normCastExt
has type
Std.Tactic.NormCast.NormCastExtension
but instance
Lean.MetaEval Std.Tactic.NormCast.NormCastExtension
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
Is there a way I can print it out to see how my declarations affect its value, or is there another way I should be investigating this?