Re: [Hol-info] Instantiating existentials under existentials

[Ramana K. <Ram...@cl...>]

Depending on the body of the existential, you might be better off not
mentioning any of the variable names and instead using
part_match_exists_tac and a "pattern" that both picks out the `y` and
provides the `5`.

On 22 March 2016 at 07:12, Ramana Kumar <Ram...@cl...> wrote:

> Yes there is:
> CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5`
>
> On 22 March 2016 at 07:08, Magnus Myreen <mo...@ca...> wrote:
>
>> Hi hol-info,
>>
>> Quick question: is there a tactic for instantiating a nested
>> existential based on a name? Example: for a goal such as
>>
>>   ?x y z. ... y ...
>>
>> I want to use a tactic foo_tac `y` `5` and get:
>>
>>   ?x z. ... 5 ...
>>
>> Is there such a foo_tac tactic? I suspect this functionality is there
>> somewhere already. If not, then I'll implement it.
>>
>> Note: I don't need the advanced feature of being able to instantiate
>> it with `x+z+1` where the variables refer to the other existentially
>> quantified variables.
>>
>> Many thanks,
>> Magnus
>>
>>
>> ------------------------------------------------------------------------------
>> Transform Data into Opportunity.
>> Accelerate data analysis in your applications with
>> Intel Data Analytics Acceleration Library.
>> Click to learn more.
>> http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
>> _______________________________________________
>> hol-info mailing list
>> hol...@li...
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>