Re: [Hol-info] How to eliminate existential quantifier in a goal about list?

Better, in my opinion, is to use e( qexists_tac`0` ); which parses the quotation in the context of the goal, so you don't need to give an explicit type annotation. On 13 April 2017 at 14:11, Thomas Tuerk wrote: > Hi Liu, > > you have realLib open. "0" can be parsed as

Re: [Hol-info] How to eliminate existential quantifier in a goal about list?

Hi Liu, you have realLib open. "0" can be parsed as either a real or a num. That's why you get the warning that two resolutions are possible. The "EXISTS_TAC ``0``" fails, because ``0`` is parsed as a real, while you need a num. An explicit type annotation does the trick: So use e (EXISTS_TAC

[Hol-info] How to eliminate existential quantifier in a goal about list?

Hi， I have a question about eliminating the existential quantifier.As follows, load "realLib"; open listTheory; Datatype `coordinate = <|x_axis: real; y_axis: real; z_axis: real|>`; val p = ``p: coordinate list``; (*goal1*) g `^p <> [] ==> ?c:coordinate. MEM c ^p`; e (RW_TAC list_ss