Stream: Coq users

Topic: ✔ Tactic returning a proof witness and existential variables


view this post on Zulip Pierre Vial (Aug 24 2021 at 09:45):

Hi,
[EDIT (solved): apparently, it was just a matter of putting a clearat a wrong place]
I'm writing a Ltactactic tacsuch that:

I'm pretty sure that step 1 and 2 are good.
When I try to do this on an example of the form:
assert (try1 := ltac:(tac foo bar bar' ) ).
I obtain the following error:
Cannot infer an existential variable of type "?T" in environment: H := forall (x : Set) (x0 x1 : x) (x2 x3 : list x), x0 :: x2 = x1 :: x3 -> x0 = x1 /\ x2 = x3 /\ True : Prop t : H
If I specify that the type of try1 is H, I get the error: The reference H was not found in the current environment.
Is there a direct workaround to solve this ?

view this post on Zulip Notification Bot (Aug 24 2021 at 15:01):

Christian Doczkal has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC