You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The let rec keyword is parsed to a list of equation expressions. However, the equation handler equation_desc on zparser.mly has no support for refinement types and the following example does not compile:
let rec (a, b) : btype {box(expression)} = body in output
For reference, take a look at the simple_type and type_expression implementation for refinement types on zparser.mly. We need to add a similar pattern match construct for equations.
[Easier task] - Add a pattern match for refinement types on the parse equation handler. This will enable refinement type annotation for let rec expressions.
The text was updated successfully, but these errors were encountered:
jlvargasme
changed the title
Add refinement type support for equations
[Summer] Add refinement type support for equations
May 2, 2022
The
let rec
keyword is parsed to a list of equation expressions. However, the equation handlerequation_desc
onzparser.mly
has no support for refinement types and the following example does not compile:let rec (a, b) : btype {box(expression)} = body in output
For reference, take a look at the
simple_type
andtype_expression
implementation for refinement types onzparser.mly
. We need to add a similar pattern match construct for equations.[Easier task] - Add a pattern match for refinement types on the parse equation handler. This will enable refinement type annotation for let rec expressions.
The text was updated successfully, but these errors were encountered: