Re: [isabelle] Real number numeric literals in Isabelle
From: cl-isabelle-users-bounces at lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Norbert
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
>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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and