Re: [Hol-info] e (qexists_tac `0`); won't parse

[Michael N. <mic...@an...>]

Do you see the same output in the example as per the Tutorial?  If you have

  ∃x’. x = 0 ∨ x’ = 0

then I’d be very surprised if qexists_tac `0` failed.

Best wishes,
Michael

On 21 Mar 2022, at 03:47, Brian Milnes <bri...@gm...<mailto:bri...@gm...>> wrote:

Folks,

 What is wrong with the Euclid example?

 Pg 30 of the tutorial?

 The `0` won't parse and I get

> e (qexists_tac `0`);
OK..

Exception raised at Tactical.Q_TAC:
No parse for quotation
Exception-
   HOL_ERR
     {message = "No parse for quotation", origin_function = "Q_TAC",
      origin_structure = "Tactical"} raised

 Thanks, Brian


--
Take em to church Billy (Payne). - Paul Barrere
_______________________________________________
hol-info mailing list
hol...@li...<mailto:hol...@li...>
https://lists.sourceforge.net/lists/listinfo/hol-info