package coq-mathcomp-dioid

  1. Overview
  2. No Docs
Dioid

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. L
    Lucien Rakotomalala <lucien.rakotomalala@onera.fr>
  2. P
    Pierre Roux <pierre.roux@onera.fr>

Maintainers

  1. P
    Pierre Roux <pierre.roux@onera.fr>

Sources

0.1.tar.gz
sha256=3700493956f6c2bc4e0f2374160f078e60366f1f98bf10960e110512096c4c52

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 oppositve 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:dioid

Published: 31 Aug 2020

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.9" & < "1.13~"
  2. coq >= "8.10" & < "8.14~"

Dev Dependencies

None

Used by

None

Conflicts

None