Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] basic example causes error message

Email Gateway (Aug 19 2022 at 07:52):

From: Gergely Buday <gbuday@gmail.com>
Hi,

I have installed the official Isabelle release, and tried the
following example from Programming and Proving:

theory MyList
imports Main
begin
datatype ’a list = Nil | Cons ’a "’a list"
fun app :: "’a list => ’a list => ’a list" where
"app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"
fun rev :: "’a list => ’a list" where
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
value "rev(Cons True (Cons False Nil))"
end

now, at the datatype declaration jedit shows an error sign and the output says

Outer syntax error: name declaration expected,
but bad input ’a was found

What is the problem here?

• Gergely

Email Gateway (Aug 19 2022 at 07:54):

From: Peter Lammich <lammich@in.tum.de>
Are you sure you use the right tick character?
It should be 'a, not ’a.

Peter

p.s. This always happens to me when copy-pasting material from pdf, as
most pdf-viewers seem to use OCR to reconstruct the text from the
graphics.

Last updated: Apr 24 2024 at 04:17 UTC