Hi Liu,
For any n, you can indeed get the nth element of x by using EL.
What do you want to do with it?
I can try to explain the behaviour you reported, in case it helps.
val _= type_abbrev("numlist",``: num list``);
val x = ``x: numlist``;
val n_element = ``!n. EL n ^x``;
This attempted term, n_element, is not well-typed because:
> type_of ``EL n ^x``;
val it = ``:num``:hol_type
but the body of a universally quantified term must be a proposition, i.e.,
have type ``:bool``, not ``:num``.
Cheers,
Ramana
On 6 April 2017 at 12:54, Liu Gengyang <2015200...@mail.buct.edu.cn> wrote:
>
> Hi Micheal,
>
> I am so sorry that I seem to have sent a blank email.
>
> I want to express: for any n,I can get the nth element of x.
>
> val _= type_abbrev("numlist",``: num list``);
> val x = ``x: numlist``;
>
> I want to keep x is x, so I add a "^" before x
>
> val n_element = ``!n. EL n ^x``;
>
> and the system prompt "Type inference failure",I don't know why there is
> such a mistake. If I delete "!n":
>
> val n_element = ``EL n ^x``;
>
> It's succeed.Maybe I have some wrong understanding about universal
> quantifier.
>
> Thanks for your reply.
>
> Best,
>
> Liu
>
> -----Original Messages-----
> *From:*michael.norr...@data61.csiro.au
> *Sent Time:*2017-04-06 11:42:56 (Thursday)
> *To:* 2015200...@mail.buct.edu.cn, hol-info@lists.sourceforge.net
> *Cc:*
> *Subject:* Re: [Hol-info] A question about EL in listTheory.
>
>
> 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 <2015200...@mail.buct.edu.cn>
> *Date: *Thursday, 6 April 2017 at 12:55
> *To: *hol4_QA <hol-info@lists.sourceforge.net>
> *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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
