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 <[email protected]<mailto:[email protected]>> 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 [email protected]<mailto:[email protected]> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
