Stream: Beginner Questions

Topic: why the following eisbach method definition fail to parse?

view this post on Zulip Jason Hu (Sep 16 2022 at 13:40):

Hi all, I am not sure how to add a case in match?

the following code is almost a copy from eisbach doc:

method foo =
(match conclusion in ‹P ∧ Q› for P Q ⇒ ‹fail› | ‹R› for R ⇒ ‹prop_solver›)

if I remove everything after | then it parses. I am using the latest release of Isabelle.

view this post on Zulip Mathias Fleury (Sep 16 2022 at 13:45):

For reasons that are beyond me, it is not a pipe |, but a ¦ (\<bar>)

view this post on Zulip Mathias Fleury (Sep 16 2022 at 13:46):

and bar is printed as a pipe to maximize confusion (I got hit by this too)

view this post on Zulip Jason Hu (Sep 16 2022 at 13:55):

oh boi

view this post on Zulip Mathias Fleury (Sep 16 2022 at 17:57):

this might be necessary to distinguish between the | from match and the | (or) from tactics

view this post on Zulip Mathias Fleury (Sep 16 2022 at 18:04):

In general: remember that the source code of the tutorials is present in the Isabelle distribution (here: ~~src/Doc/Eisbach), so you can check directly the sources

Last updated: Nov 13 2025 at 08:29 UTC