Re: [isabelle] Error in Eisbach syntax diagram

Hi Wolfgang,

On 7 Oct 2020, at 07:26, Wolfgang Jeltsch <wolfgang-it at<mailto:wolfgang-it at>> wrote:

According to my understanding, the syntax diagram on page 1 of The
Eisbach User Manual says that an alternative in an invocation of the
`match` method must have exactly one pattern.

Looking at page 1, I don’t think the diagram says that. In fact it doesn’t say anything about “match” that I can see. It mainly says what is possible on the left hand of the equality sign in a method declaration. The right-hand side of the equality is just “method” (which does include match).

On page 7 (Chapter 2, match method), the syntax diagram specifies multiple patterns separated by “|”, which I think is correct.

However, several patterns
are possible, as for instance the first example on page 3 witnesses.

Is it this example? (page 3, witnesses)

method intro_ex for Q :: ′a ⇒ bool and y :: ′a = (rule exI [where P = Q and x = y])

It doesn’t use the “match” method. Do you mean the “for .. and ..” part?


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