Coq-Equations
Coq-Equations copied to clipboard
mattam82
A function definition package for Coq
I have found at least two examples where it returns the anomaly "List.chop" when something is not fully applied A minimal example where not all variables have been given: ```...
It seems that somehow Equations is not able to handle a particular application where the decreasing argument is a Prop but the result is meaningful. A reproduction is the following...
Given the inductive ``` Inductive eq' : forall (A: Type), A -> A -> Prop := | eq_refl' : forall (A: Type) (a: A), eq' A a a | eq_funext'...
I am investigating whether we could remove Bvector (vectors of bool) from stdlib. It looks like Equations was needlessly depending on it while only using the polymorphic Vector. I imagine...
Here's my best effort attempt at minimizing the example: ```coq From Equations Require Import Equations. Inductive Ki : Type := | Star : Ki. Inductive Ty : Type := |...
The [inspect pattern](https://github.com/mattam82/Coq-Equations/blob/7863db39705298aeabfe6cc7f7518d30ec96b246/examples/Basics.v#L506-L538) relies on the following definition and notation: ```coq Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. Notation "x...
A warning > Automatically inlined signature for type vec. Use [Derive Signature for vec.] to avoid this. Is triggered when deriving NoConfusionHom but not when deriving NoConfusion. I would have...
I found a weird behavior with depelim. In the code below, depelim keeps inverting the equality ``` Section Foo. Context (x y : vec nat 2). Definition foo (H :...
Lately, I have written a Coq project to verify a data structure using Equations. This data structure is called catenable deques, a queue supporting push, pop, inject (push at the...
