Stream: MetaCoq

Topic: extends


view this post on Zulip Jason Gross (Nov 27 2022 at 18:44):

What is extends / extends_decls used for? It's kind of an awkward notion, because it doesn't guarantee semantic extension (if any kernel names are duplicated, the result of lookup can change even in an extension), and neither is semantic extension sufficient for extends_decls (because order may change). I'm wondering if it can be replaced with something that has a definite relationship to semantic extension

view this post on Zulip Yann Leray (Nov 27 2022 at 20:16):

From what I saw, both are mostly used in pair with wf / on_global_env, which ensures no duplicates. Also, I don't think the order is that significant, since the declarations should pretty much always appear in the order of the input (I guess there may be some caveats when more than one file is involved)


Last updated: Feb 04 2023 at 01:03 UTC