[isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?
- To: usr Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?
- From: Gottfried Barrow <igbi at gmx.com>
- Date: Mon, 01 Sep 2014 22:11:05 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
The canonical way in the HOL sources, when there's no need for a total
function, is to not cover all the cases, like "last", which is not
covered for :
primrec last :: "'a list => 'a" where
"last (x # xs) = (if xs =  then x else last xs)"
I've been doing that kind of thing, but it occurred to me that I could
put "undefined" to good use, to get rid of the warnings, like this:
datatype fooD = Bar | BarC "nat option"
fun BarC_get :: "fooD => nat" where
"BarC_get Bar = undefined"
|"BarC_get (BarC None) = undefined"
|"BarC_get (BarC (Some n)) = n"
Instead of like the above:
fun BarC_get2 :: "fooD => nat" where
"BarC_get2 (BarC (Some n)) = n"
Is there some, good, mysterious reason why I shouldn't do this to get
rid of the warnings?
This archive was generated by a fusion of
Pipermail (Mailman edition) and