cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Implement parser that supports unsupported features

Open ordinarymath opened this issue 3 months ago • 2 comments

When writing CakeML code/porting code from other ml implementations one would accidentally use features that CakeML currently doesn't support. This issue is not proposing to implement these features but make the parser successfully parse said features and output error messages along the lines that the feature isn't supported.

ordinarymath avatar Sep 12 '25 18:09 ordinarymath

Three major features I can think of:

  1. Datatype definition syntax (C of t1 * t2 * ...)
  2. Records
  3. Functors and signatures

Anything else?

wildptr avatar Sep 19 '25 12:09 wildptr

open infix

ordinarymath avatar Sep 19 '25 13:09 ordinarymath