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
For consistency, I would expect that when we have u : Level then inside q we could use $u to refer to it. This seems to work sometimes, whereas at other times we need u inside q. The inconsistency is confusing. For example:
For consistency, I would expect that when we have
u : Level
then insideq
we could use$u
to refer to it. This seems to work sometimes, whereas at other times we needu
insideq
. The inconsistency is confusing. For example:The text was updated successfully, but these errors were encountered: