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 approach I plan to take is to pre-analyze all function definitions and store the corresponding z3 types in the context, so when the inferencer encounters the g function call (whose definition didn't appear yet) it will have its type already in the context.
The problem with this is that it will allow some incorrect programs to type, like the following one:
Example
The approach I plan to take is to pre-analyze all function definitions and store the corresponding z3 types in the context, so when the inferencer encounters the
g
function call (whose definition didn't appear yet) it will have its type already in the context.The problem with this is that it will allow some incorrect programs to type, like the following one:
Because by the time
f
is called,g
wouldn't have appeared yet.What do you think? Do you think the above example is tolerable? Can we consider it as a normal run-time error that is not type-related?
The text was updated successfully, but these errors were encountered: