Tomás Díaz
Tomás Díaz
Following from the issue [211](https://github.com/mattam82/Coq-Equations/issues/211), I tried rewriting my code to simplify it but I keep getting the ``` Error: Illegal application: The Xth term has type "A" which should...
I came across this error while trying to prove the following : ``` Lemma filter_preserves_non_redundancy flt queries : are_non_redundant queries -> are_non_redundant (γ__φ flt queries). Proof. apply_funelim (γ__φ flt queries)...
I came up with this error : ``` Error: Anomaly "Uncaught exception Invalid_argument("index out of bounds")." Please report at http://coq.inria.fr/bugs/. ``` I am not sure how to make a simple...
Hi, I was trying to define a function with some nested `where` clauses, in which one of them uses a wf recursion. I get the following error when trying to...
I got the following error while trying to admit an obligation: ``` Error: Anomaly "more than one statement." Please report at http://coq.inria.fr/bugs/. ``` I was doing something of the following...
Hi, I was trying to define a function and tried to admit the obligation and got a `Error: Anomaly "Uncaught exception Environ.NotEvaluableConst(0)." Please report at http://coq.inria.fr/bugs/.`. I noticed there was...
I defined a wf recursive function and repeated two cases mistakenly, which resulted in an error msg: ``` Anomaly "File "printing/ppconstr.ml", line 399, characters 14-20: Assertion failed." Please report at...
Hi, I was trying to change the moving speed of my simulated Ergo Jr but it is not reflected in the simulator. It does change it, as in... If I...
**esy version:** 0.6.12 **Operating System:** macOS Big Sur 11.6.1 **Issue:** Cannot install any new dependency. Build failing with this message, regardless of the package I'm adding: ```bash info building @opam/easy-format@opam:1.3.3@f5b11eb6...
Hi, I'm having some memory leak issues due to byte[] being copied when passing it back. For now I'm directly calling the GC to cleanup but I was wondering if...