Re: [isabelle] Real number numeric literals in Isabelle


-----Original Message-----
From: Brian Huffman [mailto:brianh at] 
Sent: Saturday, December 17, 2005 3:20 AM

>In Isabelle the power operator (^) takes a natural number as its second
argument. Since there are no negative naturals, >-6::nat is actually
interpreted as being equal to 0::nat. So 2 * 10 ^-6 is probably not what
you want; you can use 2 / 10^ >6 instead.

>Isabelle currently does not have support for decimal point syntax for
numbers like 1.3 (although it would be possible to  >add support for it
by writing some ML code). You could just translate 1.3 as 13/10, and
longer decimals like
>123.4567 as 1234567/10^4.

I didn't think of this.

>Check out the file HOL/Real/Float.thy in the Isabelle sources. There is
a constant float :: int * int => real that might 
>be close to what you want (but it uses base 2 instead of base 10 for
the exponent).


>- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.