1
$\begingroup$

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?

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.