# Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"

In higher-order logic, as in first-order logic, all functions are total. This is a fact of model theory. It doesn't imply that a partial function is “made total” in any explicit way, and it is obvious that no uniform definition of hd[] is possible. All that you can say for certain is that this value has the correct type and is equal to itself.
Larry Paulson
On 2 Sep 2010, at 20:31, Bart Kastermans wrote:
> 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.

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