[isabelle] solving error
I began to read Isabelle tutorial. I proceed
program bellow step by step, but it show
me error. Does anybody know how to
*** Inner lexical error at: @ ys = ys
*** Failed to parse proposition
*** At command "primrec".
datatype 'a list = Nil
| Cons 'a "'a list"
primrec app :: "'a list => 'a list => 'a list"
" @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list => 'a list" where
"rev  = " |
"rev (x # xs) = (rev xs) @ (x # )"
value "rev (True # False # )"
This archive was generated by a fusion of
Pipermail (Mailman edition) and