Problem solved. It turns out that an integer numeral is actually an
application of int_of_num anyway (when non-negative). So the trick is to
include integerTheory.NUM_OF_INT in your compset. Annoyingly, this theorem
is not included in intReduce.int_compset().
On Tue, Apr 15, 2014 at 7:46 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>wrote:
> Turns out I was confused again, this time by commonUnif$Num shadowing
> integer$Num.
>
> The thing I actually want is something to reduce ``Num n`` to ``n`` where
> n is a non-negative numeral (it has different types in the two quotations).
> That's probably a bit more involved and maybe doesn't exist yet.
>
>
> On Tue, Apr 15, 2014 at 7:42 AM, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk>wrote:
>
>> oops, the title of this thread should be NUM_OF_INT conversion, and then
>> no conversion is needed: it's just a rewrite... still, it should be a
>> rewrite that's in the int compset surely?
>>
>>
>> On Tue, Apr 15, 2014 at 7:30 AM, Ramana Kumar
>> <ramana.ku...@cl.cam.ac.uk>wrote:
>>
>>> I'm about to write a conversion to reduce terms of the form Num(&n)
>>> where n is a ground non-negative integer. But I would expect such a thing
>>> to already exist somewhere - does anyone know where?
>>>
>>> I notice that EVAL does not reduce Num(&1) - is there something I can
>>> load that will make it do so?
>>>
>>
>>
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
