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:
``CASE x OF [ |||. (NONE, []) ~> 0 ]``
fails with the following error:
Don't expect to find a > in this position after a ~
at line 25, character 40 and at line 25, character 39.
Exception-
HOL_ERR
{message =
"at line 25, character 39:\nDon't expect to find a > in this
position after a ~\nat line 25, character 40 and at line 25, character
39.\n",
origin_function = "Absyn", origin_structure = "Absyn"} raised
Would you have any ideas on how to enable the custom "CASE .. OF [ .. ]"
syntax?
Cheers,
Armaël
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports.http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
