1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
fullname: Finite maps
shortname: finmap
organization: math-comp
opam_name: coq-mathcomp-finmap
community: false
action: true
coqdoc: false
synopsis: >-
Finite sets, finite maps, finitely supported functions
description: |-
This library is an extension of mathematical component in order to
support finite sets and finite maps on choicetypes (rather that finite
types). This includes support for functions with finite support and
multisets. The library also contains a generic order and set libary,
which will be used to subsume notations for finite sets, eventually.
authors:
- name: Cyril Cohen
initial: true
- name: Kazuhiko Sakaguchi
initial: false
opam-file-maintainer: Cyril Cohen <cyril.cohen@inria.fr>
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
file: CECILL-B
supported_coq_versions:
text: Coq 8.16 to 8.20
opam: '{ (>= "8.16" & < "8.20~") | (= "dev") }'
tested_coq_opam_versions:
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.16'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.17'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.0" & < "2.3~") | (= "dev") }'
description: |-
[MathComp ssreflect 2.0 to 2.2](https://math-comp.github.io)
namespace: mathcomp.finmap
keywords:
- name: finmap
- name: finset
- name: multiset
documentation: |-
## Documentation
The documentation is available in the header of the file.
This library will be integrated to the mathematical components
library in the near future.
## Related work
This library was developed independently but inspired from
[Pierre-Yves Strub's
library](https://github.com/strub/ssrmisc/blob/master/fset.v), from
[Christian Doczkal's
library](https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html)
and from Beta Ziliani's work (no reference provided so far).
Another alternative is [Arthur Azevedo de Amorim extensional
structures library](https://github.com/arthuraa/extructures).
## Acknowledgments
Many thanks to Kazuhiko Sakaguchi (for the order library now moved to
the main math-comp repository) and to [various
contributors](https://github.com/math-comp/finmap/graphs/contributors)
|
