[isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
I am playing with defining some recursive functions and proving their
properties, I don't understand some of what I am seeing. The following
questions, I think, will help me move in the right direction.
In HOL/List.thy we see the definition:
hd :: "'a list => 'a" where
"hd (x # xs) = x"
The tutorial states all functions defined this way must be total, so
somehow hd is made total. thm hd_def gives information on where to look,
but that theory file (SList.thy) is apparently only for "historical
interest". This makes me think there should be a better way to find out
how this function is made total.
value "hd ";
normal_form "hd ";
evaluate to themselves. So does
value "if true then [2,3] else [4,5]"
How do I force evaluation of those? The first I have no idea what it
should evaluate to; the last should be [2,3].
Thanks for any help,
Werner Herzog: the birds here ... they don't sing ... they scream in
A Better Tea Timer (version 0.1).
This archive was generated by a fusion of
Pipermail (Mailman edition) and