Zulip Chat Archive

Stream: general

Topic: instance used


petercommand (Nov 18 2018 at 16:51):

is there some way to show which instance (of a class) is actually used in a definition? If I use set_option trace.class_instances true, it lists lots of possible instances, but I only want the actual instance used

Mario Carneiro (Nov 18 2018 at 16:52):

I sometimes grep the output to remove lines immediately followed with failed defeq

Mario Carneiro (Nov 18 2018 at 16:53):

but of course you can always just look at the term

petercommand (Nov 18 2018 at 16:53):

just look at the term?

petercommand (Nov 18 2018 at 16:53):

yeah, I can grep the output

Mario Carneiro (Nov 18 2018 at 16:54):

Just trigger the instance search manually. For example:

set_option pp.implicit true
#check (by apply_instance : preorder int)
-- @partial_order.to_preorder ℤ
--   (@ordered_comm_group.to_partial_order ℤ
--      (@ordered_ring.to_ordered_comm_group ℤ
--         (@linear_ordered_ring.to_ordered_ring ℤ
--            (@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
--               (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
--                  int.decidable_linear_ordered_comm_ring))))) :
--   preorder ℤ

petercommand (Nov 18 2018 at 16:55):

Ah..that works great! Thanks!

Kenny Lau (Nov 18 2018 at 17:15):

alternatively:

set_option pp.implicit true
#check (infer_instance : preorder int)
/-
@infer_instance (preorder ℤ)
  (@partial_order.to_preorder ℤ
     (@ordered_comm_group.to_partial_order ℤ
        (@ordered_ring.to_ordered_comm_group ℤ
           (@linear_ordered_ring.to_ordered_ring ℤ
              (@linear_ordered_comm_ring.to_linear_ordered_ring ℤ
                 (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ℤ
                    int.decidable_linear_ordered_comm_ring)))))) :
  preorder ℤ
-/

Last updated: Dec 20 2023 at 11:08 UTC