The operator precedence of |> (opt_map) is currently set at 54, lower than the operator precedence of |< (opt_pred), which is at 55, leading to the expression P |< f |> g not being well-formed. This expression, by type, should unambiguously be equivalent to P |< (f |> g). If we were to make the precedence of |> stronger (that is, make its number higher than the number for |<), then this expression would parse successfully. This change does not break Reader_Option_Monad, where these constants are defined, but might require an update to the proofs.
The operator precedence of
|>(opt_map) is currently set at 54, lower than the operator precedence of|<(opt_pred), which is at 55, leading to the expressionP |< f |> gnot being well-formed. This expression, by type, should unambiguously be equivalent toP |< (f |> g). If we were to make the precedence of|>stronger (that is, make its number higher than the number for|<), then this expression would parse successfully. This change does not breakReader_Option_Monad, where these constants are defined, but might require an update to the proofs.