The API for terms, contexts, lifting, substitution, replacing is sometimes appealing (e.g. I find
constr.mli rather nice to some extent) but also sometimes deceiving (e.g. a function exists on
econstr but not on
constr, or vice-versa, or the terminology is inconsistent, or the function is not in the expected module, ...).
Is there some consensus or maybe some ongoing project on stabilizing an API which we are satisfied with?
A prior question is maybe about how we resolve the conflict between not having more than what the kernel needs in the kernel API and the convenience of having a unique name space for everything about terms or contexts (e.g.
open Constr on
open EConstr on
econstr), for everything about lift and substitutions (e.g.
module CVars = Vars on
open EConstr providing
Personally, I don't care about having functions with a clear semantics and documentation in the kernel even if not directly used by the kernel, but a system of reexport in the style of
CList which includes
Nameops which includes
Name is also ok.
To start with, splitting
termops.mli into what pertains to
econstr and what pertains to
constr would be nice. It could proceed by splitting the file, or by having two submodules, or by moving the
econstr part to
EConstr.Vars and having
Another current limitation is
inductiveops.mli which does not directly support
I would support having an
etermops or the like, at least I think that would be good for plugin writers. If that can be moved to EConstr then even better in my opinion. We should also have a wrapper
einductiveops for sure, I think most of the administrative back and forth between e- and non-e things in equations is because we lack this.
Last updated: Jun 08 2023 at 04:01 UTC