[isabelle] Type annotations for tuple abstractions



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




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