@Pierre-Marie Pédrot : we recently discussed in the performance thread the symbol management functions for managing delta reduction symbol lists. Since I need this desperately I also started to work on it, but wanted to avoid too much double work.
What I currently have is:
This is intended to analyze the situation for a specific goal at hand. My next step would be a function which looks recursively in a term (looks also in the definitions of transparent constants found in the term).
May I ask what you are working on? I hope more on extracting symbol lists from modules as we discussed in Sophia Antipolis.
Last updated: Feb 04 2023 at 22:29 UTC