added type information to produce the expected result with value
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 07 Oct 2014 16:17:23 +0100
changeset 24 789ade899a53
parent 23 768851ac930b
child 25 a2a7f65f538a
added type information to produce the expected result with value
thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Tue Oct 07 12:48:56 2014 +0100
+++ b/thys/CountSnoc.thy	Tue Oct 07 16:17:23 2014 +0100
@@ -19,9 +19,9 @@
   if x = y then Suc(count_list x xs) 
   else count_list x xs)"
 
-value "count_list 1 [1,1,1]"
-value "count_list 1 [2,2,2]"
-value "count_list 2 [2,2,1]"
+value "count_list (1::nat) [1,1,1]"
+value "count_list (1::nat) [2,2,2]"
+value "count_list (2::nat) [2,2,1]"