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.
On 2 Sep 2010, at 20:31, Bart Kastermans wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and