On 3/03/12 12:29 AM, Wishnu Prasetya wrote:
> Hey guys,
>
> When playing with HOL recently I had a problem in rewriting a set
> comprehension. BETA_CONV refuses to reduce this:
>
> --`{x | x >0} x`--
>
> I use pred_set, so that should be the same as --`(\x. x>0) x`--.
>
> Bug or feature?
Even when using pred_set, the term
{ x | x > 0 }
is not syntactically equal to (\x. x > 0).
Rather it is equal to
GSPEC (\x. (x, x > 0))
The simplifier will automatically handle terms such as
``y IN {x | x > 0}``
and you should definitely avoid getting into the situation where you
have a set comprehension applied to an argument (as above).
I hope this helps.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Virtualization & Cloud Management Using Capacity Planning Cloud computing makes use of virtualization - but cloud computing also focuses on allowing computing to be delivered as a service. http://www.accelacomm.com/jaw/sfnl/114/51521223/
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
