Stream: metaprogramming / tactics
Topic: Dependencies and local defs
Jannis Limperg (Oct 13 2020 at 09:58):
I have a PR, #4602, which deals with dependencies between hypotheses. One point I'm not sure about, and on which I would appreciate your feedback, is the handling of local defs. Copy-pasting the relevant comment from the PR:
The interesting case is this:
n : N m : N := n h : m > 0
h depend on
n? Currently, the PR says no. This simplifies the implementation since "depends on" can be decided by a simple syntactic occurrence check.
kdepends_on infamously ignores local defs altogether. However, I find all this semantically fishy.
Gabriel Ebner (Oct 13 2020 at 09:59):
It should depend on it. Dependency should be a transitive relation.
Last updated: May 09 2021 at 22:13 UTC