coq-addition-chains.opam

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/coq-community/hydra-battles"
dev-repo: "git+https://github.com/coq-community/hydra-battles.git"
bug-reports: "https://github.com/coq-community/hydra-battles/issues"
license: "MIT"

synopsis: "Exponentiation algorithms following addition chains in Coq"
description: """
Addition chains are algorithms for computations of the p-th power of some x, 
with the least number of multiplications possible. This development provides
a few implementations of addition chains in Coq, including proofs of their
correctness."""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.14"}
  "coq-paramcoq" {>= "1.1.3"}
  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
  "coq-mathcomp-algebra"
]

tags: [
  "category:Mathematics/Combinatorics and Graph Theory"
  "keyword:addition chains"
  "keyword:exponentiation algorithms"
  "logpath:additions"
]
authors: [
  "Pierre Castéran"
  "Yves Bertot"
]