Stream: Coq users

Topic: Symbol management functions


view this post on Zulip 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:

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