Email Gateway (Aug 22 2022 at 13:51): Email Gateway (Aug 22 2022 at 13:51):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear syntax experts,
It seems as if I cannot add type annotations to whole abstraction patterns in
abstractions. Here is a minimal example:
type_synonym pair = "nat × nat"
term "%(a, b) :: pair. a + b"
Here, Isabelle complains about a parse error at "." However,
term "%(a :: nat, b :: nat). a + b"
works as expected. I would prefer to use the type synonyms in the annotations because they
convey more meaning than the plain component types.
Am I just making a silly mistake or are type annotations for composite patterns not
supported? If not, why not? What would need to change to support this?
Is it only me or would other people find such annotations useful, too?
Side remark: The same parsing errors also occur in other places where tuple syntax is
supported, e.g.
set comprehensions "{(a, b) :: pair. a + b > 10}"
big operators "∑(a, b) :: pair. a + b"
Best,
Andreas
Last updated: Apr 25 2024 at 16:19 UTC