Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Eisbach syntax specification to restrictive?


view this post on Zulip Email Gateway (Aug 14 2023 at 15:38):

From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hello!

The railroad diagram for the match method in the Eisbach tutorial says
that for each case there can be only a single pattern. However, the
example right after the railroad diagrams has multiple patterns for a
single case, which are separated by and. Does the railroad diagram
need updating?

Also I understand that fact names and the multi argument are probably
not allowed when matching a term, as this term might not denote a fact
and it is only a single term, not a list. Is this understanding correct?

All the best,
Wolfgang


Last updated: Apr 28 2024 at 20:16 UTC