finmap
finmap copied to clipboard
math-comp
Finite sets, finite maps, multisets and generic sets
Dear Barbichu, I started working with your order.v file and I realized that there are some missing construction. I'm willing to contribute, but I'm really scared by all these Canonical...
This branch/PR is to record the tentative port of `set.v` to MathComp 2. At the time of this writing, it is based on PR #84 (the port of finmap to...
It'd be nice if `fset_sub_finType` would be made a coercion. ``` Coercion fset_sub_finType : finSet >-> finType. ```
In Coq 8.14 (rc1), I am getting this: ``` File "./finmap/finmap.v", line 752, characters 0-186: Error: Library Coq.Program.Tactics has to be required first. ``` Indeed adding `Require Coq.Program.Tactics.` at the...
The following script showcases some unfortunate notation behaviors (on the current coq.dev and finmap.dev) ```coq From mathcomp Require Import all_ssreflect finmap. Open Scope fset_scope. Lemma fsetIsep (T : choiceType) (A...
The github "Description" for `finmap` says "Finite sets, finite maps, multisets and order". It should maybe be "Finite sets, finite maps, and multisets" now that `order` is in MathComp.
I'm opening this issue to track the result of a recent discussion on Gitter. Coq 8.11.1 release broke `coq-mathcomp-finmap` on opam and some other packages that depend on it: `coq-mathcomp-multinomials`,...
In file https://github.com/math-comp/finmap/blob/master/order.v: > latticeType == the type of distributive lattices I.E.: all lattices are assumed to be distributive. There is a lot to say on non-distributive lattices. I'd love...
Hi, Is there a reason that a {fset T} with T a fintype isn't considered a fintype ?
