meta.yml

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)