Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: generating a has_coe_to_fun in a tactic


view this post on Zulip Yakov Pechersky (Jan 07 2021 at 23:50):

How does one make this work?

import data.equiv.basic
import tactic

open tactic

set_option trace.app_builder true

example : true := by do
  try_inst  mk_app `has_coe_to_fun [`(equiv.perm )],
  trace try_inst,
  admit

I've been trying things like:

  sic  mk_instance_cache `(equiv.perm ),
  (sic, coe_inst)  sic.get `has_coe_to_fun,

but that get fails.

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 00:12):

Very difficult, but there's an implicit second universe parameter, so this works:

example : true := by do
  try_inst  pure `(has_coe_to_fun.{1 1} (equiv.perm )),
  trace try_inst,
  admit

view this post on Zulip Simon Hudon (Jan 08 2021 at 00:29):

get would need to generate meta universe variables for every universe that cannot be inferred from the arguments.

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 00:29):

For some reason,

cls  get_classes `(@equiv.{1 1}  )

fails to get has_coe_to_fn too, with app builder complaining that [app_builder] failed to create an 'has_coe_to_fun'-application, there are missing implicit arguments. But what would those implicit arguments be? Another ?

view this post on Zulip Simon Hudon (Jan 08 2021 at 00:30):

I think those would be universe parameters

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 00:31):

For which things? Other than the already specified Sort 1 and Sort 1, what else is implicit?

view this post on Zulip Simon Hudon (Jan 08 2021 at 00:33):

#check @has_coe_to_fun
has_coe_to_fun : Sort u_1  Sort (max u_1 (u_2+1))

This means that the function type that you're coercing to can be in different universes from the argument


Last updated: May 09 2021 at 23:10 UTC