Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Dependencies and local defs


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

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?

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