Stream: Coq users

Topic: Symbol management functions

Michael Soegtrop (Sep 08 2022 at 14:00):

@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:

• a function which extracts all constants from a term
• a function which filters a list of constants vs. a list of module path prefixes

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: Apr 20 2024 at 01:41 UTC