Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Rob Arthan <rda <at> lemma-one.com>
Subject: HOL Light set comprehensions
Newsgroups: gmane.comp.mathematics.hol
Date: Friday 22nd November 2013 16:33:48 UTC (over 4 years ago)
This is idle curiosity on my part about HOL Light: why are the constants
that support set comprehensions defined in such a way that the parser has
to generate an invisible bound variable? This results in surprising
behaviour like:

# `{x | x > 9}` = `{x | x > 9}`;;
val it : bool = false

HOL4 defines set comprehensions the way I would expect (using a single
constant GSPEC with type 'a -> 'b # BOOL -> 'b -> BOOL) and doesn't need to
insert any invisible bound variables.

Regards,

Rob.
 
CD: 2ms