Hi Liu,
I don't know EXTENCE_TAC. I would have used EXISTS_TAC. This shound not
depend on whether "a" is a record type or not. So something like:
Q.EXISTS_TAC `EL n A`
It might be worth looking at REFINE_TAC to partially instantiate the
record and quantifier heuristics (QI_ss) to split the
Hi,
I have a question as follow:
load "realLib";
open listTheory;
Datatype `coordinate = <|x_axis: real; y_axis: real; z_axis: real|>`;
val A = ``A: coordinate list``;
g `^A <> [] ==> !n. ?a. a.x_axis <= (EL n A).x_axis`;
- e(RW_TAC list_ss []);
OK..
1 subgoal:
> val it =
?a.
