Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Set notation "extremely ambiguous"?


view this post on Zulip Email Gateway (Aug 18 2022 at 10:19):

From: "Dr. Brendan Patrick Mahony" <Brendan.Mahony@dsto.defence.gov.au>
I am encountering an interesting phenomena with HOL's set notation.

Apparently there is a parse conflict between the finite set notation eg

{f x y}

and the set comprehension notation eg

{f x y | x y. p x y}

At some point as the grammar get larger (possibly to do with the
number of infix operators),
this results in a plethora warnings: "### Currently parsed expression
could be extremely ambiguous."

Is this slowing things down significantly?

Any suggestions for fixing the syntax?

Brendan


Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au

Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.

IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.


Last updated: May 03 2024 at 04:19 UTC