Théo Winterhalter
Théo Winterhalter
I hope I am not missing something, but when I just type `\`, it does not realize I want to insert a symbol. I need to open the palette to...
It seems that defining actions directly in an `effect` or `layered_effect` results in an error message. Below is an example which works: ```fstar module MWE let wpost a = a...
This problem is probably not specific to vscoq (I think it is the same with Proof General) but I believe it is probably solved at the editor level. Currently when...
Follow up from coq-community/vscoq-legacy#42. I think it would be really nice to have the goals and hypotheses in separate frames (or I don't know how to call those areas with...
Perhaps I'm missing something but the autocompletion for `Arguments` yields: ```coq Arguments {{qualid}} {{possibly_bracketed_idents …}}. ``` It does not even select the bracketed strings that you have to modify. As...
Hard to minimise so the error can be [checked out at this commit](https://github.com/TheoWinterhalter/template-coq/blob/3b2b1018de25aea291675fc2fcbc6a89ae0875c6/pcuic/theories/PCUICParallelReductionConfluence.v#L2449). After the use of `funelim`, I have an ill-typed induction hypothesis in one of my goals. ```...
I have an effect where parameters are also universe polymorphic, and since F* requires me to have only one universe variable, I have to set two of them to be...
When you use `Program` or `Equations` and you have generated obligations, vscoq doesn't seem to display the obligations anywhere, so you have to guess how many there are left.
Hi, thanks for the great package. I was wondering if there was any way to add some attributes to the `` that gets generated by your package. I mean, something...
We propose an extension of Coq with user-defined rewrite rules, following our work on formalising rewrite rules in MetaCoq and the paper [The Taming of the Rew]. [Rendered here]. [The...