Stream: Is there code for X?
Topic: class instance in hypothesis
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
d were achieved through
intros on a Pi type. Thanks!
Eric Wieser (Jan 13 2021 at 23:43):
apply_instance will close that goal, as I think will
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.
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?
Eric Wieser (Jan 13 2021 at 23:47):
Can you give a #mwe?
Eric Wieser (Jan 13 2021 at 23:48):
(at a guess, you're looking for tactic#resetI)
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.
Chase Norman (Jan 13 2021 at 23:52):
introsI was exactly what I was looking for, thanks!
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