Re: [isabelle] Real number numeric literals in Isabelle



-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Norbert
Schirmer
Sent: Friday, December 16, 2005 10:52 AM


>Why do you think this measure is bad?

I do not know if the measure is bad. My problem is actually that I do
not really understand how measure works so it took me sometime to think
of this one...

I was wondering how someone else with experience would use measure on
real numbers. 


>HOL is a logic of total functions. So you cannot just leave out cases.
But since every type in HOL has at least one       >member,  there is
indeed a default value called arbitrary. You can return it instead of
-1, to emphasise that this is a >"dead end"...


Ah ha. I will try this.

>   Norbert

Thanks,

Primrose





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