Coq-Equations
Coq-Equations copied to clipboard
mattam82
A function definition package for Coq
Hello, ``` From Equations Require Import Equations. CoInductive foo : Type := FOO1. Equations ex (x: foo) : nat := ex FOO1 := 2. ``` ``` Error: Anomaly "Uncaught exception...
In the following I expected `f n` to be rewritten by `funelim (f n)`, but it only changes `n`. ``` From Equations Require Import Equations. Set Implicit Arguments. Set Contextual...
It would be great to have a variant of `funelim` like `induction foo as [... | ... | ...]` or better yet for compatibility with the Mathcomp style an option...
Here's the example, the failure at Equations seems like it should be a proof-obligation instead ``` From Coq Require Import Fin List Program. From Equations Require Import Equations. Notation fin...
As a consequence an `open Termops` becomes useless in `eqdec.ml`. (`Termops` keeps the variants on `constr`.) To be merged synchronously with coq/coq#15565.
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...
```coq From Equations Require Import Equations. Set Equations Transparent. Inductive term := | tBox | tConstruct (ind : nat) (c : nat) | tConst (kn : nat). Equations eta_exp_discr (t...
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. ```...
Sorry for a non-informative title. I stumbled upon this trying to add another constructor to the type o intristically-typed expressions in `examples/definterp.v`. I added the following constructor: ``` | Y...
