Tomás Díaz
Tomás Díaz
I rewrote my code to not use any recursive call and I am still getting the error message, so I am guessing it has nothing to do with it haha....
So far I've noticed it is happening whenever there is a 3rd `where` clause (even if it is not being called). Simple examples such as the following : ``` Equations...
I ended up collapsing the three `where` clauses into a single one, which itself has another nested `where` clause (2 `where` clauses in total). Thing is that this version is...
Just wondering, I've been using this one which is "old" but I am not sure if it's ok or not haha (it works for me at least). https://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v#L43
Ups, actually I just repeated the exact same code twice and still got the same error msg.
I changed the definition so I no longer do that `with` clause over `ty` in the nested `where` clause and I no longer get the error message. I basically lifted...
I actually get the error in [212](https://github.com/mattam82/Coq-Equations/issues/212) with this new definition 😄.
Not entirely sure if related or not, but I got a stack overflow while trying to prove an obligation for a wf definition: Goal : ``` queries_size φ < query_size...
I redefined it so I no longer have this situation but I recall that rewriting with the equations would just give me the expected result. In this case: `1 +...
Having a similar issue in OS X (esy v.0.6.12), although when running the command in the isolated environment: `esy b dune build @fmt --auto-promote`. The error is the following: ```shell...