Zulip Chat Archive
Stream: maths
Topic: norm_cast trace
Jakob von Raumer (Sep 28 2022 at 15:14):
Is there a way to see which lemmas norm_cast used? The trace seems little informative.
Gabriel Ebner (Sep 28 2022 at 15:17):
set_option trace.simplify.rewrite true
Jakob von Raumer (Sep 28 2022 at 15:29):
But it seems like norm_cast rewrites along more than that?
Gabriel Ebner (Sep 28 2022 at 15:42):
Yes, I believe the numeral rewriting is not done via the simplfiier. There is also set_option trace.norm_cast true which might be helpful.
Last updated: Dec 20 2023 at 11:08 UTC