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, privacy policy and cookie policy

Browse other questions tagged or ask your own question.