# [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.
`
Q1:
In HOL/List.thy we see the definition:
primrec
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.
`
Q2:
value "hd []";
and
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,
Best,
Bart
--
http://bartk.nl/
@kasterma, http://twitter.com/kasterma
Werner Herzog: the birds here ... they don't sing ... they scream in
agony.
blaginations, http://kasterma.wordpress.com
A Better Tea Timer (version 0.1).

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