instance used

Stream: general

[petercommand]

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]

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

[Mario Carneiro]

but of course you can always just look at the term

[petercommand]

just look at the term?

[petercommand]

yeah, I can grep the output

[Mario Carneiro]

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]

Ah..that works great! Thanks!

[Kenny Lau]

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 ℤ
-/