1 theory CountSnoc

     2 imports Main

     3 begin

     4 

     5 datatype 'a myList = Nil | Cons 'a "'a myList"

     6 

     7 fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where

     8 "app_list Nil ys = ys" |

     9 "app_list (Cons x xs) ys = Cons x (app_list xs ys)"

    10 

    11 fun rev_list :: "'a myList \<Rightarrow> 'a myList" where

    12 "rev_list Nil = Nil" |

    13 "rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"

    14 

    15 (*

    16 fun count_list :: "'a \<Rightarrow> 'a myList \<Rightarrow> nat" where

    17 "count_list x [] = 0" |

    18 "count_list x (y#xs) = (

    19   if x = y then Suc(count_list x xs) 

    20   else count_list x xs)"

    21 *)

    22 

    23 fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where

    24 "count_list x [] = 0" |

    25 "count_list x (y#xs) = (

    26   if x = y then Suc(count_list x xs) 

    27   else count_list x xs)"

    28 

    29 <<<<<<< local

    30 value "count_list 1 [1,1,0]"

    31 value "count_list 1 [2,2,2]"

    32 value "count_list 2 [2,2,1]"

    33 =======

    34 value "count_list (1::nat) [1,1,1]"

    35 value "count_list (1::nat) [2,2,2]"

    36 value "count_list (2::nat) [2,2,1]"

    37 >>>>>>> other

    38  

    39