Jason Hu (Sep 16 2022 at 13:40): 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.
Mathias Fleury (Sep 16 2022 at 13:45):For reasons that are beyond me, it is not a pipe |, but a ¦ (\<bar>)
Mathias Fleury (Sep 16 2022 at 13:46):and bar is printed as a pipe to maximize confusion (I got hit by this too)
Jason Hu (Sep 16 2022 at 13:55):oh boi
Mathias Fleury (Sep 16 2022 at 17:57):this might be necessary to distinguish between the | from match and the | (or) from tactics
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: Dec 21 2024 at 16:20 UTC