Re: [Hol-info] Instantiating existentials under existentials

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

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
>