Dependencies and local defs

Stream: metaprogramming / tactics

[Jannis Limperg]

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

Does 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.

Opinions?

[Gabriel Ebner]

It should depend on it. Dependency should be a transitive relation.