Re: [isabelle] Real number numeric literals in Isabelle
From: Brian Huffman [mailto:brianh at cse.ogi.edu]
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and