coq-mathcomp-dioid.opam

opam-version: "2.0"
version: "dev"
maintainer: [
  "Pierre Roux <pierre.roux@onera.fr>"
]

homepage: "https://github.com/math-comp/dioid"
dev-repo: "git+https://github.com/math-comp/dioid.git"
bug-reports: "https://github.com/math-comp/dioid/issues"
license: "CECILL-B"

build: [
  [make "-j%{jobs}%"]
]
install: [make "install"]

depends: [
  "coq" { >= "8.16" & < "8.18~" }
  "coq-mathcomp-algebra" { >= "2.0" & < "2.1~" }
  "coq-mathcomp-classical" { >= "1.0" & < "1.1~" }
  "coq-hierarchy-builder" { >= "1.4.0" }
]
synopsis: "Dioid"
description: """
Definitions of the algebraic structure of dioid following the style of
ssralg in the Mathcomp library.

The main algebraic structures defined are:
* semirings: rings without opposite for the additive law
* dioids: idempotent semirings (i.e., forall x, x + x = x)
* complete dioids: dioids whose canonical order (x <= y wen x + y = y)
  yields a complete lattice
* commutative variants (multiplicative law is commutative)

More details can be found in comments at the beginning of each file.
"""

tags: [
  "keyword:dioid"
  "keyword:semiring"
  "keyword:complete dioid"
  "category:Miscellaneous/Coq Extensions"
  "logpath:mathcomp.dioid"
]
authors: [
  "Lucien Rakotomalala <lucien.rakotomalala@onera.fr>"
  "Pierre Roux <pierre.roux@onera.fr>"
]
#url {
#  src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz"
#  checksum: "sha256=TODO curl -L archive | sha256sum"
#}