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. a.x_axis <= (EL n A).x_axis
------------------------------------
A <> []
: proof
Now I want to use EXTENCE_TAC to instantiate "a", but I don't know how to do
it, because "a" is a record type. Could anyone help me?
Thanks,
Liu------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
