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
With the notion of Extensions/Plugins from #214 , the additional_builtins of the Typer module is redundant and can be removed. However it would not be nice to users to remove it right away, and should instead be removed in a few versions (maybe after being deprecated ?).
The text was updated successfully, but these errors were encountered:
Actually there is a difference between additional_builtins and extensions: additional_builtins give access to the state, while extensions do not. I'm not sure if this functionality is needed (in fact I think it is not -- in any case we don't use it in Alt-Ergo) but something to keep in mind maybe.
With the notion of Extensions/Plugins from #214 , the
additional_builtins
of theTyper
module is redundant and can be removed. However it would not be nice to users to remove it right away, and should instead be removed in a few versions (maybe after being deprecated ?).The text was updated successfully, but these errors were encountered: