Re: [isabelle] solving error



Your code lacks the definitions of the notations involving "[]" "#" and "@" that are used in the equations.
In your context Isabelle just doesn't know what [],#,@ mean.
You have two choices:
Either you tell Isabelle about the used notations by adding the parts
("[]")
(infixr "#" 65)
(infixr "@" 65)
you left out from the tutorial
or you use the explicit names changing the equations to something like:

primrec app :: "'a list =>  'a list =>  'a list"
where
"app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"



I hope this helps, these additional notations might be a bit confusing at the beginning.

Am 24.01.2011 12:31, schrieb Novio:
Hi,
I began to read Isabelle tutorial. I proceed
program bellow step by step, but it show
me error. Does anybody know how to
solve it?
Thanks

ERROR
*** Inner lexical error at: @ ys = ys
*** Failed to parse proposition
*** At command "primrec".

PROGRAM
theory ToyList
imports Datatype
begin

datatype 'a list = Nil
| Cons 'a "'a list"

primrec app :: "'a list =>  'a list =>  'a list"
where
"[] @ 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 # [])"
end







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.