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
This could be accepted, but F* complains that "Recursive functions must be introduced at arrow types", I believe due to taking bool as the annotation and ignoring the two binders. Dropping the annotations makes it work.
The text was updated successfully, but these errors were encountered:
This allows to have an abbreviated expected type as long as it reduces
to an arrow.
Use N.get_n_binders () to obtain the needed amount of binders without
over flattening.
Fixes#2895
This could be accepted, but F* complains that "Recursive functions must be introduced at arrow types", I believe due to taking
bool
as the annotation and ignoring the two binders. Dropping the annotations makes it work.The text was updated successfully, but these errors were encountered: