François Pottier
François Pottier
I see. But in my real-world application, which is Iris, the "typing judgement" is not inductively defined. I have a semantic definition of it, and a bunch of lemmas that...
Anyway, this is instructive. It is a fundamental complexity issue of which I was unaware until now.
I believe that the proof term (which Coq must type-check) is a DAG of linear size, but is viewed by the Coq type-checker as a tree of quadratic size, because...
> Can you write a "type checker with side conditions"? @JasonGross Perhaps...? I do not know this technique and, based on what you wrote, I do not get the idea....
Thanks for the pointers! Regarding your thesis, in 3.1.4, I do not get the idea of switching from `is_related` to `is_related_elim`. Why is the second representation more efficient?
Thanks, I am looking forward to trying this out. When (in which version) will it be released?
Your argument that "we need to traverse the term to detect sharing" does not necessarily convince me. In the example that I proposed at the beginning of this PR, the...
I am interested in reading this documentation, but I was not able to build it; checking out this PR and attempting to build the manual results in a type error....
Thanks @gasche . Here are some remarks about the new section 12.5.1 of the manual. I hope this can be useful. I would suggest writing "parameterized" instead of "parametrized". "Functions...
Thanks for your contribution! I don't know who has time to test / authority to merge? (I have not had time to test, and I don't know whether I have...