dolmen icon indicating copy to clipboard operation
dolmen copied to clipboard

Remove the Typer's addition builtins following the merge of Extensions/Plugins

Open Gbury opened this issue 9 months ago • 1 comments

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 ?).

Gbury avatar Mar 18 '25 16:03 Gbury

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.

bclement-ocp avatar Mar 18 '25 17:03 bclement-ocp