@ppedrot: A late remark about last week discussion on linking constants at require-time. Would there be disadvantages at the end at linking lazily (using an option mutable field in Const
/Ind
/Construct
constructors)? How much could we expect to gain?
Last updated: Oct 13 2024 at 01:02 UTC