Ah ok; thanks. Thank explains! --wish.
> 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
>
>
------------------------------------------------------------------------------
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
