# HG changeset patch # User paulson # Date 866463851 -7200 # Node ID bea2faf1641d82df6fb8c0ec220b07f8fb332e27 # Parent d68dbb8f22d3f53b8120bbdca1f7624009ae22bb Replacing the primrec definition of "length" by a translation to the built-in "size" function diff -r d68dbb8f22d3 -r bea2faf1641d src/HOL/List.thy --- a/src/HOL/List.thy Fri Jun 13 10:35:13 1997 +0200 +++ b/src/HOL/List.thy Mon Jun 16 14:24:11 1997 +0200 @@ -16,7 +16,6 @@ concat :: 'a list list => 'a list foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b hd :: 'a list => 'a - length :: 'a list => nat set_of_list :: 'a list => 'a set list_all :: ('a => bool) => ('a list => bool) map :: ('a=>'b) => ('a list => 'b list) @@ -53,6 +52,11 @@ Cons "[| a: A; l: lists A |] ==> a#l : lists A" +(*Function "size" is overloaded for all datatypes. Users may refer to the + list version as "length".*) +syntax length :: 'a list => nat +translations "length" => "size" + primrec hd list "hd([]) = arbitrary" "hd(x#xs) = x" @@ -87,9 +91,6 @@ primrec foldl list "foldl f a [] = a" "foldl f a (x#xs) = foldl f (f a x) xs" -primrec length list - "length([]) = 0" - "length(x#xs) = Suc(length(xs))" primrec concat list "concat([]) = []" "concat(x#xs) = x @ concat(xs)"