Zulip Chat Archive

Stream: Is there code for X?

Topic: class instance in hypothesis


view this post on Zulip Chase Norman (Jan 13 2021 at 23:41):

Is it possible to have the lean type system recognize class instances in hypotheses? In tactic mode I have the following error:

failed to synthesize type class instance for
V X : Type,
a : fintype X,
b : nonempty X,
c : fintype V,
d : nonempty V,
P : Profile V X
 nonempty V

Clearly, the hypothesis d has the required information. How can I make it accessible via tactic mode? Variables a through d were achieved through intros on a Pi type. Thanks!

view this post on Zulip Eric Wieser (Jan 13 2021 at 23:43):

apply_instance will close that goal, as I think will assumption

view this post on Zulip Chase Norman (Jan 13 2021 at 23:45):

Unfortunately, this is not a goal. It is an error that arises when I attempt to use a function that requires a nonempty fintype as input.

view this post on Zulip Chase Norman (Jan 13 2021 at 23:46):

is there a way that I can have it surface these errors as a goal instead of failing?

view this post on Zulip Eric Wieser (Jan 13 2021 at 23:47):

Can you give a #mwe?

view this post on Zulip Eric Wieser (Jan 13 2021 at 23:48):

(at a guess, you're looking for tactic#resetI)

view this post on Zulip Bryan Gin-ge Chen (Jan 13 2021 at 23:48):

You might be able to use @ in front of that function and supply the instance manually.

view this post on Zulip Chase Norman (Jan 13 2021 at 23:52):

introsI was exactly what I was looking for, thanks!

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 00:21):

In general, the type class system knows about everything "before the colon" (in a theorem statement) but doesn't know about things which appear after the colon, or which show up later. The ...I tactics are a way of inserting stuff which shows up in other ways, into the type class system.


Last updated: May 07 2021 at 23:11 UTC