Coq-Equations

Coq-Equations copied to clipboard

Incorrect universe error

1

I have a recursive function using a non-trivial measure that has been successfully defined before using a functional and `well_founded_induction_type`, that I've translated to Equations. However, I get the following...

palmskog

Anomaly Invalid_argument ("index out of bounds")

2

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...

TDiazT

Anomaly "Uncaught exception Not_found"

3

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...

TDiazT

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...

TDiazT

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...

TDiazT

Obligation Tactic impacts `Program Fixpoint`

7

It seems `Equations` modified the obligation tactic so that it brings some unexpected impact to `Program Fixpoint`. ``` Show Obligation Tactics. (* Program obligation tactic is program_simpl (globally defined) *)...

HuStmpHrrr

simp diverges in presence of match

8

simp diverges, see example below (Coq 8.9). ``` From Coq Require Import Arith Lia. From Equations Require Import Equations. Equations? Mod (x y : nat) : nat by wf x...

gert-smolka

fatal error when generating _equation lemmas

12

Following error was generated: ``` Error: Anomaly "File "src/principles_proofs.ml", line 285, characters 21-27: Assertion failed." Please report at http://coq.inria.fr/bugs/. ``` This happens when I mix with patterns and where clauses...

HuStmpHrrr

Anomaly File printing

2

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...

TDiazT

with patterns and where clauses are mutually exclusive

4

It appears that with patterns and where clauses are mutual exclusive. Namely ```coq Equations foo arg1 : ret := foo pat1 with (bar arg2) => { blah } where baz...

HuStmpHrrr