As discussed here https://github.com/FStarLang/FStar/pull/2816, sometimes we want to have a refinement on the LHS of a non-dependent tuple, but the parser will still take (x:a{p x}) & b to be dependent. This PR changes this behavior to make parenthesis break the binding on a tuple type.
(Notably function types like (x:a) -> Tot (b x) do bind across a parenthesis.)
Regressions in F* are minor, checking everest now.
As discussed here https://github.com/FStarLang/FStar/pull/2816, sometimes we want to have a refinement on the LHS of a non-dependent tuple, but the parser will still take
(x:a{p x}) & bto be dependent. This PR changes this behavior to make parenthesis break the binding on a tuple type.(Notably function types like
(x:a) -> Tot (b x)do bind across a parenthesis.)Regressions in F* are minor, checking everest now.