Thomas has it right. The behaviour whereby dtcase prints as case is a bug that
I will try to get around to fixing at some point.
Note that this is all with respect to HOL as you check it out from master on
github, not Kananaskis-10.
Michael
On 28/07/2016, 08:54, "Thomas Tuerk"
Hi Armaël,
the syntax you use and that is still used in patternMatchesExamples.ML
was the one used before Michaels changes and the recent merge of the
branch you mention.
I'm not too sure myself, how to use the new one and what the new syntax
is exactly. From looking at Michael's commits and the
Hi all,
I'm trying to use the pattern_matches/ library of HOL4 (that has been merged
relatively recently). Basically, I tried running the very first examples
of the
example file (src/pattern_matches/patternMatchesExamples.ML), and it
seems to
fail to parse the custom syntax for PMATCH:
