Hi,
I want to use EL in listTheory to get the nth element in a list. For example,
val _= type_abbrev("numlist",``: num list``);
val x = ``x: numlist``;
val n_element = ``!n. EL n x``;
type_of n_element;
val it = ``:bool`` : hol_type
I am wondering why the type of n_element is bool rather than num? How can I get
the nth element in a list?
Regards，
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
