Stream: Coq devs & plugin devs

Topic: Explanation of kernel/esubst.ml


view this post on Zulip Mathis Bouverot-Dupuis (May 17 2024 at 22:21):

I'm looking at explicit substitutions (kernel/esubst.ml). In the .mli there are some typing explanations for substitutions, but I have a hard time understanding the formalism from the comments and code alone. Is there some place I can find some more explanations (paper, talk, etc) ?


Last updated: Oct 13 2024 at 01:02 UTC