thys/CountSnoc.thy
changeset 24 789ade899a53
parent 23 768851ac930b
child 25 a2a7f65f538a
equal deleted inserted replaced
23:768851ac930b 24:789ade899a53
    17 "count_list x [] = 0" |
    17 "count_list x [] = 0" |
    18 "count_list x (y#xs) = (
    18 "count_list x (y#xs) = (
    19   if x = y then Suc(count_list x xs) 
    19   if x = y then Suc(count_list x xs) 
    20   else count_list x xs)"
    20   else count_list x xs)"
    21 
    21 
    22 value "count_list 1 [1,1,1]"
    22 value "count_list (1::nat) [1,1,1]"
    23 value "count_list 1 [2,2,2]"
    23 value "count_list (1::nat) [2,2,2]"
    24 value "count_list 2 [2,2,1]"
    24 value "count_list (2::nat) [2,2,1]"
    25  
    25  
    26 
    26 
    27 
    27 
    28 
    28 
    29 
    29