coq-ext-lib
coq-ext-lib copied to clipboard
coq-community
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
The Coq team released Coq `8.16+rc1` on June 01, 2022. The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**. It can be delayed in case of...
Not sure why the definition of `sequence` breaks...
The issue is similar to https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and mentioned in https://github.com/coq-community/coq-ext-lib/issues/121 and https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r783571726.
I recently discovered this wonderful option: [`Set Typeclass Strict Resolution`](https://coq.inria.fr/distrib/current/refman/addendum/type-classes.html#coq:flag.Typeclasses-Strict-Resolution), which would help avoid infinite loop problems such as that motivating https://github.com/coq-community/coq-ext-lib/pull/106. > When looking for unifications of a goal...
My original suggestion: _I have seen many projects putting together their own Monad stuff in Coq. Sometimes poorly. Ideally, they should all use ExtLib, but I think it has more...
The `EqvWF_Build` instance appears to lead astray typeclass resolution when performing unrelated rewrites. Consider the following code snippet relying on itrees: ``` From ITree Require Import ITree Eq.Eq. Goal forall...
@gmalecha the goals of ext-lib and stdlibpp seem similar. I know you are using both. Would it make sense to try to merge some common parts? There also seems to...
Monoids in `coq-ext-lib` are defined as follow: https://github.com/coq-community/coq-ext-lib/blob/ee71d144bd2a171532d9243198538c93aebb8a58/theories/Structures/Monoid.v#L11-L14 Is there a special reason that the definition is a `Record` rather than a `Class`? I know that, under the hood, they...
Metadata
Owner
Metadata
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]