EL is indeed the right constant to use:
> EVAL ``EL 3 [4;5;6;7;8]``;
val it = |- EL 3 [4; 5; 6; 7; 8] = 7: thm
I don’t know what you’re trying to express by writing ``!n. EL n x``. The
English reading of that term would be “for all n, the nth element of x is
true”. (Remember that the ‘!’ is the universal (“for all”) quantifier.)
Note also that writing
val x = ``x:numlist``
does *not* affect the way x is parsed in other terms. In particular, when you
wrote ``!n. EL n x``, the x in that quotation will have been given the type
:bool list. You can see this by setting the show_types reference:
> show_types := true;
val it = () : unit
> val x = ``x : num list``;
val x = ``(x :num list)``: term
> val n_element = ``!n. EL n x``;
val n_element =
``∀(n :num). EL n (x :bool list)``:
term
I hope this helps,
Michael
From: Liu Gengyang <[email protected]>
Date: Thursday, 6 April 2017 at 12:55
To: hol4_QA <[email protected]>
Subject: [Hol-info] A question about EL in listTheory.
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
