Email Gateway (Aug 18 2022 at 16:49): Email Gateway (Aug 18 2022 at 16:49):From: Novio <novio@azet.sk>
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
Email Gateway (Aug 18 2022 at 16:49):From: bnord <bnord01@googlemail.com>
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.
Last updated: Apr 20 2024 at 12:26 UTC