Zulip Chat Archive
Stream: general
Topic: type class trace dump
Johan Commelin (Aug 07 2018 at 06:25):
Is this expected behaviour?
import linear_algebra.multivariate_polynomial set_option trace.class_instances true instance foobar : comm_ring (mv_polynomial ℕ ℚ) := by apply_instance
I won't copy-paste the trace here, it is pretty long.
Last updated: Dec 20 2023 at 11:08 UTC